Proofgold Term Root Disambiguation

∀ x0 x1 . SNoLt 0 x1 ⟶ ordinal (SNoLev x1) ⟶ SNo x1 ⟶ x1 = 0 ⟶ ∀ x2 : ο . x2

as obj
-

as prop
d43ff..^{Conj_SNo_pos_eps_Le__1__3}

theory
HotG

stx
b740c..

address
TMXhP..^{Conj_SNo_pos_eps_Le__1__3}