Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ setexp (SNoS_ omega) omega ⟶ ∀ x1 . x1 ∈ setexp (SNoS_ omega) omega ⟶ (∀ x2 . x2 ∈ omega ⟶ ∀ x3 . x3 ∈ omega ⟶ SNoLt (ap x0 x2) (ap x1 x3)) ⟶ ∀ x2 : ο . (SNoCutP (prim5 omega (ap x0)) (prim5 omega (ap x1)) ⟶ SNo (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1))) ⟶ SNoLev (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1))) ∈ ordsucc omega ⟶ SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1)) ∈ SNoS_ (ordsucc omega) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (ap x0 x3) (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1)))) ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1))) (ap x1 x3)) ⟶ x2) ⟶ x2

as obj
-

as prop
3ca0b..^{SNo_approx_real_lem}

theory
HotG

stx
64dcd..

address
TMPrs..^{SNo_approx_real_lem}