Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLt x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ SNoL x1 ⟶ x3 ∈ SNoR x0 ⟶ x2) ⟶ (x0 ∈ SNoL x1 ⟶ x2) ⟶ (x1 ∈ SNoR x0 ⟶ x2) ⟶ x2

as obj
-

as prop
ffc0b..^{SNoLt_SNoL_or_SNoR_impred}

theory
HotG

stx
fd8fe..

address
TMRDw..^{SNoLt_SNoL_or_SNoR_impred}