NF weak partition development: NominalAlphaRepairedBase001023Addc.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfAddc (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A B) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWrex y A (Compiler.CompactSourceSyntax.synWrex z B (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv y) (SemanticCore.Class.cv z)) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))))))))

Checked nominal proof certificate identified upstream as nominal_df_addc.

Equations

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