Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ real ⟶ ∀ x1 . x1 ∈ real ⟶ SNoLt x0 x1 ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x0 x2) (SNoLt x2 x1))

as obj
-

as prop
ced79..

theory
HotG

stx
aa676..

address
TMbcx..