Proofgold Term Root Disambiguation

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

as obj
-

as prop
b651e..^{ordinal_ordsucc_In_eq}

theory
HF

stx
82de5..

address
TMQLf..^{ordinal_ordsucc_In_eq}