Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ setexp (SNoS_ omega) omega ⟶ ∀ x2 . x2 ∈ setexp (SNoS_ omega) omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (ap x1 x3) x0) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt x0 (add_SNo (ap x1 x3) (eps_ x3))) ⟶ (∀ x3 . x3 ∈ omega ⟶ ∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x1 x4) (ap x1 x3)) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt x0 (ap x2 x3)) ⟶ (∀ x3 . x3 ∈ omega ⟶ ∀ x4 . x4 ∈ x3 ⟶ SNoLt (ap x2 x3) (ap x2 x4)) ⟶ x0 = SNoCut (prim5 omega (ap x1)) (prim5 omega (ap x2)) ⟶ x0 ∈ real

as obj
-

as prop
fca80..^{SNo_approx_real}

theory
HotG

stx
64dcd..

address
TMFFQ..^{SNo_approx_real}