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 (add_SNo x2 1)))) (SNoLe (ap x1 (add_SNo x2 1)) (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
0d70c..^{real_complete2}

theory
HotG

stx
c59bb..

address
TMM2d..^{real_complete2}