Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ SNoLt 0 (ordsucc x0)

as obj
-

as prop
7e3b0..^{ordinal_ordsucc_pos}

theory
HotG

stx
e9e67..

address
TMHv7..^{ordinal_ordsucc_pos}