Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x0 ⟶ x1 ∈ x0 ⟶ or (ordsucc x1 ∈ x0) (x0 = ordsucc x1)

as obj
-

as prop
0c19e..^{ordinal_ordsucc_In_eq}

theory
HotG

stx
18c18..

address
TMHGn..^{ordinal_ordsucc_In_eq}