Proofgold Term Root Disambiguation

(∀ x0 x1 x2 x3 x4 . (∀ x5 . x5 ∈ x1 ⟶ SNo x5) ⟶ SNo (SNoCut x0 x1) ⟶ (∀ x5 . x5 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x5) ⟶ (∀ x5 . SNo x5 ⟶ (∀ x6 . x6 ∈ x0 ⟶ SNoLt x6 x5) ⟶ (∀ x6 . x6 ∈ x1 ⟶ SNoLt x5 x6) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x5) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x5)) ⟶ SNo x4 ⟶ SNoLt x4 (SNoCut x0 x1) ⟶ (∀ x5 . x5 ∈ x0 ⟶ SNoLt x5 x4) ⟶ not (∀ x5 . x5 ∈ x1 ⟶ SNoLt x4 x5)) ⟶ ∀ x0 : ο . x0

as obj
-

as prop
74d4d..

theory
HotG

stx
6bc83..

address
TMWxn..