Proofgold Proposition

∀ x0 . SNo x0 ⟶ SNoLt 0 x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ SNoLt 0 x2 ⟶ and (SNo (x1 x2)) (mul_SNo x2 (x1 x2) = 1)) ⟶ SNoCutP (famunion omega (λ x2 . ap (SNo_recipaux x0 x1 x2) 0)) (famunion omega (λ x2 . ap (SNo_recipaux x0 x1 x2) 1))

type
prop

theory
HotG

name
SNo_recipaux_lem2

proof
PUewm..

Megalodon
SNo_recipaux_lem2

proofgold address
TMQQU..^{SNo_recipaux_lem2}

creator
27779 PrQUS../21830..

owner
27779 PrQUS../21830..

term root
38996..