Proofgold Proposition

∀ x0 . SNo x0 ⟶ ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ x1 x3 = x2 x3) ⟶ ∀ x3 . nat_p x3 ⟶ SNo_recipaux x0 x1 x3 = SNo_recipaux x0 x2 x3

type
prop

theory
HotG

name
SNo_recipaux_ext

proof
PUewm..

Megalodon
SNo_recipaux_ext

proofgold address
TMXPY..^{SNo_recipaux_ext}

creator
27779 PrQUS../3dc5d..

owner
27779 PrQUS../3dc5d..

term root
b2de4..