NF weak partition development: NominalAlphaRepairedBase001006If.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfIf (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) ph.neg))))

Checked nominal proof certificate identified upstream as nominal_df_if.

Equations

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