Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ (∀ x1 . x1 ∈ SNoS_ (SNoLev x0) ⟶ SNoLt x1 x0) ⟶ ordinal x0

as obj
-

as prop
f28b9..^{SNo_max_ordinal}

theory
HotG

stx
2cf07..

address
TMJBD..^{SNo_max_ordinal}