NF weak partition development: NominalNFLiteralXpViaCompletenessDev003.
theorem
NFChoice.DirectNominalPrf.Nominal.NFLiteralXpViaCompletenessDev003.axXpFv
(x y z w t : SemanticCore.Var)
(_hxy : x ≠ y)
(_hxz : x ≠ z)
(_hxw : x ≠ w)
(_hxt : x ≠ t)
(_hyz : y ≠ z)
(_hyw : y ≠ w)
(_hyt : y ≠ t)
(_hzw : z ≠ w)
(_hzt : z ≠ t)
(_hwt : w ≠ t)
:
(NFLiteralHandlers.axXpGoal x y z w t).fv ⊆ {x}
noncomputable def
NFChoice.DirectNominalPrf.Nominal.NFLiteralXpViaCompletenessDev003.axXp
(x y z w t : SemanticCore.Var)
(hxy : x ≠ y)
(hxz : x ≠ z)
(hxw : x ≠ w)
(hxt : x ≠ t)
(hyz : y ≠ z)
(hyw : y ≠ w)
(hyt : y ≠ t)
(hzw : z ≠ w)
(hzt : z ≠ t)
(hwt : w ≠ t)
:
NPrf (NFLiteralHandlers.axXpGoal x y z w t)
Proof-translation construction identified upstream as axXp.
Equations
- One or more equations did not get rendered due to their size.