NF weak partition development: NominalAlphaRepairedBase001044IdReflected001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfId (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCid (Compiler.CompactSourceSyntax.synCopab x y (SemanticCore.Wff.objEq x y)))

Checked nominal proof certificate identified upstream as nominal_df_id.

Equations

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