Proofgold Term Root Disambiguation

∀ x0 x1 . SNoCutP x0 x1 ⟶ and (and (and (and (SNo (SNoCut x0 x1)) (SNoLev (SNoCut x0 x1) ∈ ordsucc (binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2)))))) (∀ x2 . x2 ∈ x0 ⟶ SNoLt x2 (SNoCut x0 x1))) (∀ x2 . x2 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x2)) (∀ x2 . SNo x2 ⟶ (∀ x3 . x3 ∈ x0 ⟶ SNoLt x3 x2) ⟶ (∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x2) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2))

as obj
-

as prop
66456..^{SNoCutP_SNoCut}

theory
HotG

stx
fab7c..

address
TMU2S..^{SNoCutP_SNoCut}