Proofgold Term Root Disambiguation

∀ x0 . SNo_ omega x0 ⟶ ∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ or (and (nIn (SNoLev x1) x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ x2 ∈ x0)) (and (SNoLev x1 ∈ x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ nIn x2 x0))

as obj
-

as prop
8fb40..

theory
HotG

stx
80e8e..

address
TMd5r..