Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ and (ordinal (SNoLev x0)) (SNo_ (SNoLev x0) x0)

as obj
-

as prop
21761..^SNoLev_prop

theory
HotG

stx
fab7c..

address
TMEuZ..^SNoLev_prop