Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ ∀ x1 : ο . (ordinal (SNoLev x0) ⟶ SNo_ (SNoLev x0) x0 ⟶ x1) ⟶ x1

as obj
-

as prop
d259b..^{SNoLev_prop_impred}

theory
HF

stx
8964b..

address
TMTQ7..^{SNoLev_prop_impred}