NF weak partition development: NAR4C068C001Part063.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfEn (x y f : SemanticCore.Var) (dv_f_x : f ≠ x) (dv_f_y : f ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as nominal_df_en.

Equations

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