NF weak partition development: NominalAlphaRepairedDfNfc001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfNfc (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnfc x A) (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A))))

Checked nominal proof certificate identified upstream as nominal_df_nfc.

Equations

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