Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2∀ x3 . nat_p x3and (ap (SNo_sqrtaux x0 x1 x2) 0ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 0) (ap (SNo_sqrtaux x0 x1 x2) 1ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 1)
type
prop
theory
HotG
name
SNo_sqrtaux_mon_lem
proof
PUewm..
Megalodon
SNo_sqrtaux_mon_lem
proofgold address
TMLAs..SNo_sqrtaux_mon_lem
creator
27779 PrQUS../7acd6..
owner
27779 PrQUS../7acd6..
term root
be3c0..