Proofgold Object

SNo_rec_i (λ x0 . λ x1 : ι → ι . SNoCut (famunion omega (λ x2 . ap (SNo_sqrtaux x0 x1 x2) 0)) (famunion omega (λ x2 . ap (SNo_sqrtaux x0 x1 x2) 1)))

type
ι → ι

theory
HotG

name
sqrt_SNo_nonneg

definition
PUewm..

Megalodon
sqrt_SNo_nonneg

proofgold address
TMF4Z..^{sqrt_SNo_nonneg}

creator
27779 PrQUS../86ac6..

owner
27779 PrQUS../86ac6..

term root
71d15..