Proofgold Term Root Disambiguation

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

as obj
-

as prop
3be24..^{SNo_max_SNoLev}

theory
HotG

stx
2cf07..

address
TMTDt..^{SNo_max_SNoLev}