Documentation

LeanPool.NFWeakPartition.NominalAlphaRepairedBase001018P6

NF weak partition development: NominalAlphaRepairedBase001018P6.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfP6 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :
Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCp6 A) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) A)))

Checked nominal proof certificate identified upstream as nominal_df_p6.

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