Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . SNo x0 ⟶ sqrt_SNo_nonneg x0 = SNoCut (famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 0)) (famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1))
type
prop
theory
HotG
name
sqrt_SNo_nonneg_eq
proof
PUewm..
Megalodon
sqrt_SNo_nonneg_eq
proofgold address
TMLkw..sqrt_SNo_nonneg_eq
creator
27779 PrQUS../d2d44..
owner
27779 PrQUS../d2d44..
term root
63c3e..