Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ SNoLev x0 ⟶ ∀ x2 : ο . (SNoCutP {x3 ∈ SNoL x0|SNoLev x3 ∈ x1} {x3 ∈ SNoR x0|SNoLev x3 ∈ x1} ⟶ binintersect x0 (SNoElts_ x1) = SNoCut {x4 ∈ SNoL x0|SNoLev x4 ∈ x1} {x4 ∈ SNoR x0|SNoLev x4 ∈ x1} ⟶ x2) ⟶ x2

as obj
-

as prop
965ec..^{restr_SNo_SNoCut}

theory
HotG

stx
705e2..

address
TMEjp..^{restr_SNo_SNoCut}