Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ (∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ and (and (and (SNo (minus_SNo x2)) (∀ x3 . x3 ∈ SNoL x2 ⟶ SNoLt (minus_SNo x2) (minus_SNo x3))) (∀ x3 . x3 ∈ SNoR x2 ⟶ SNoLt (minus_SNo x3) (minus_SNo x2))) (SNoCutP (prim5 (SNoR x2) minus_SNo) (prim5 (SNoL x2) minus_SNo))) ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ x1 ∈ SNoS_ (SNoLev x0) ⟶ and (and (SNo (minus_SNo x1)) (∀ x2 . x2 ∈ SNoL x1 ⟶ SNoLt (minus_SNo x1) (minus_SNo x2))) (∀ x2 . x2 ∈ SNoR x1 ⟶ SNoLt (minus_SNo x2) (minus_SNo x1))

as obj
-

as prop
e0a4a..^{Conj_minus_SNo_prop1__2__2}

theory
HotG

stx
202df..

address
TMbhq..^{Conj_minus_SNo_prop1__2__2}