Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ x1 ∈ SNoLev x0 ⟶ SNo_ x1 (binintersect x0 (SNoElts_ x1)) ⟶ SNo (binintersect x0 (SNoElts_ x1))

as obj
-

as prop
61455..^{Conj_restr_SNo__1__2}

theory
HotG

stx
b740c..

address
TMMhZ..^{Conj_restr_SNo__1__2}