Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ setexp real omega ⟶ ∀ x1 . x1 ∈ setexp real omega ⟶ (∀ x2 . x2 ∈ omega ⟶ and (and (SNoLe (ap x0 x2) (ap x1 x2)) (SNoLe (ap x0 x2) (ap x0 (ordsucc x2)))) (SNoLe (ap x1 (ordsucc x2)) (ap x1 x2))) ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ real) (∀ x4 . x4 ∈ omega ⟶ and (SNoLe (ap x0 x4) x3) (SNoLe x3 (ap x1 x4))) ⟶ x2) ⟶ x2

as obj
-

as prop
96392..^{real_complete1}

theory
HotG

stx
c59bb..

address
TMPoi..^{real_complete1}