Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ordsucc x0 = add_SNo 1 x0

as obj
-

as prop
36bf6..^{ordinal_ordsucc_SNo_eq}

theory
HotG

stx
b160a..

address
TMKvp..^{ordinal_ordsucc_SNo_eq}