Proofgold Proposition

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

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_restr_SNo__1__2

proofgold address
TMGAw..^{Conj_restr_SNo__1__2}

creator
35053 PrNpY../99d3f..

owner
35061 PrNpY../43fcb..

term root
ad79e..