NF weak partition development: NominalDefinitionLeafHandlersObjExtCompat001.

ax-ext is replayed in the primitive object-language presentation, while df-cleq's historical exporter-facing adapter expected the definitionally expanded class-language presentation. The variable permutation in the replay is already the right one: axExtGoal y z x binds x and compares membership in y and z.

This type-valued certificate records only the object-to-class atomic recanonicalization. It introduces no logical assumption.

def NFChoice.DirectNominalPrf.Nominal.DefinitionLeafHandlersObjExtCompat001.axExtObjClassRecanon (x y z : SemanticCore.Var) : RecanonTransportDev.TRecanonWff (NFLiteralHandlers.axExtGoal y z x) ((SemanticCore.Wff.all x ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).biimp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv z)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (SemanticCore.Class.cv z)))

Proof-translation construction identified upstream as axExtObjClassRecanon.

Equations

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

Exact source-signature adapter for the generated df-cleq call. Unlike the older dfCleqOfDV, this accepts the object-language axExtGoal y z x proof that the literal-axiom handler actually produces, transports it through the explicit certificate above, and then calls the already-audited class handler.

noncomputable def NFChoice.DirectNominalPrf.Nominal.DefinitionLeafHandlersObjExtCompat001.dfCleqOfDVObjExt (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (hAxExt : NPrf (NFLiteralHandlers.axExtGoal y z x)) (hxA : x ∉ A.fv) (hxB : x ∉ B.fv) : NPrf (ClassHandlersDev011.dfCleqGoal x A B)

Proof-translation construction identified upstream as dfCleqOfDVObjExt.

Equations

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