Documentation

LeanPool.NFWeakPartition.NominalAlphaRepairedBase001027Ncfin

NF weak partition development: NominalAlphaRepairedBase001027Ncfin.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfNcfin (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :
Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCncfin A) (Compiler.CompactSourceSyntax.synCio x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as nominal_df_ncfin.

Equations
  • One or more equations did not get rendered due to their size.
Instances For