Proofgold Proposition

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

type
prop

theory
HotG

name
SNo_sqrtaux_ext

proof
PUewm..

Megalodon
SNo_sqrtaux_ext

proofgold address
TMbw3..^{SNo_sqrtaux_ext}

creator
27779 PrQUS../d29c4..

owner
27779 PrQUS../d29c4..

term root
9e623..