Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2 ⟶ ∀ x3 . nat_p x3 ⟶ x2 ⊆ x3 ⟶ and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 x3) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 x3) 1)

type
prop

theory
HotG

name
SNo_sqrtaux_mon

proof
PUewm..

Megalodon
SNo_sqrtaux_mon

proofgold address
TMKKy..^{SNo_sqrtaux_mon}

creator
27779 PrQUS../5e81d..

owner
27779 PrQUS../5e81d..

term root
53a99..