NF weak partition development: NominalRecanonTransportCompat001.
Wff.neg is defined as implication into falsum. The original
type-valued recanonicalization relation exposes the primitive implication
constructor but omitted this derived convenience constructor, even though
the checked certificate emitter uses the corresponding Prop-valued helper.
def
NFChoice.DirectNominalPrf.Nominal.RecanonTransportDev.TRecanonWff.neg
{p q : SemanticCore.Wff}
(h : TRecanonWff p q)
:
TRecanonWff p.neg q.neg
Proof-translation construction identified upstream as neg.