Proofgold Term Root Disambiguation

∀ x0 x1 x2 . SNoLt x0 x1 ⟶ SNo x1 ⟶ SNoLev x1 = x2 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ and (and (SNo x1) (SNoLev x1 ∈ SNoLev x0)) (SNoLt x0 x1)

as obj
-

as prop
79465..^{Conj_SNo_etaE__5__1}

theory
HotG

stx
202df..

address
TMGbJ..^{Conj_SNo_etaE__5__1}