Proofgold Term Root Disambiguation

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

as obj
-

as prop
defb9..^SNoLev_prop

theory
HF

stx
8964b..

address
TMUVg..^SNoLev_prop