NF weak partition development: NominalAlphaRepairedBase001040SsetReflected001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfSset (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as nominal_df_sset.

Equations

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