Documentation

LeanPool.NFWeakPartition.NominalDefinitionLeafHandlersCanonical001

NF weak partition development: NominalDefinitionLeafHandlersCanonical001.

One canonical import surface for the only three Metamath definition labels that do not reduce to reflexivity after deep source expansion.

source
noncomputable def NFChoice.DirectNominalPrf.Nominal.DefinitionLeafHandlersCanonical001.dfClabStructural (x y : SemanticCore.Var) (p : SemanticCore.Wff) :
NPrf (ClassHandlersDev011.dfClabGoal x y p)

Proof-translation construction identified upstream as dfClabStructural.

Equations
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.Nominal.DefinitionLeafHandlersCanonical001.dfCleqOfDV (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (hAxExt : NPrf ((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)))) (hxA : x ∉ A.fv) (hxB : x ∉ B.fv) :
    NPrf (ClassHandlersDev011.dfCleqGoal x A B)

    Proof-translation construction identified upstream as dfCleqOfDV.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.Nominal.DefinitionLeafHandlersCanonical001.dfClelOfDV (x : SemanticCore.Var) (A B : SemanticCore.Class) (hxA : x ∉ A.fv) (hxB : x ∉ B.fv) :
      NPrf (ClassHandlersDev011.dfClelGoal x A B)

      Proof-translation construction identified upstream as dfClelOfDV.

      Equations
      Instances For