Proofgold Term Root Disambiguation

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

as obj
-

as prop
3849f..^ordsuccE

theory
HotG

stx
18c18..

address
TMUfs..^ordsuccE