NF weak partition development: NominalAlphaOprabCompactSupport001.
A closed structural reflexivity certificate for the three self-paired
binders and one genuinely renamed binder used by df-oprab.
def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb049ReflOnSelf3Fresh
(x y z a w : SemanticCore.Var)
(support : Finset SemanticCore.Var)
(ha : a ∉ support)
(hw : w ∉ support)
:
Checked nominal proof certificate identified upstream as nb049_reflOn_self3_fresh.