Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0)

as obj
-

as prop
ab0f7..^{ordinal_ordsucc}

theory
HotG

stx
18c18..

address
TMNpP..^{ordinal_ordsucc}