Documentation

LeanPool.NFWeakPartition.NominalAlphaRepairedBase001029Evenfin

NF weak partition development: NominalAlphaRepairedBase001029Evenfin.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfEvenfin (x n : SemanticCore.Var) (dv_n_x : n ≠ x) :
Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCevenfin (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n)))) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC0))))

Checked nominal proof certificate identified upstream as nominal_df_evenfin.

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