Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ 0 ∈ ordsucc x0

as obj
-

as prop
a0377..^{ordinal_0_In_ordsucc}

theory
HotG

stx
e9e67..

address
TMUuF..^{ordinal_0_In_ordsucc}