Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ ordinal (SNoLev x0)

as obj
-

as prop
e3541..^{SNoLev_ordinal}

theory
HF

stx
8964b..

address
TMcVA..^{SNoLev_ordinal}