NF weak partition development: NominalDefinitionRefl.

Proof-object reflexivity for class-valued definitional leaves.

noncomputable def NFChoice.DirectNominalPrf.Nominal.classEqRefl (A : SemanticCore.Class) : NPrf (SemanticCore.Wff.classEq A A)

Proof-translation construction identified upstream as classEqRefl.

Equations

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