Documentation

LeanPool.NFWeakPartition.NominalAlphaRepairedBase001024Nnc

NF weak partition development: NominalAlphaRepairedBase001024Nnc.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfNnc (y b : SemanticCore.Var) (dv_b_y : b ≠ y) :
Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCint (SemanticCore.Class.cab b (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0c (SemanticCore.Class.cv b)) (Compiler.CompactSourceSyntax.synWral y (SemanticCore.Class.cv b) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv b)))))))

Checked nominal proof certificate identified upstream as nominal_df_nnc.

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