Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0)

as obj
-

as prop
8f4aa..^{ordinal_ordsucc}

theory
HF

stx
82de5..

address
TMFrL..^{ordinal_ordsucc}