Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ SNoLe 0 x0 ⟶ SNoCutP (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1)) ⟶ (∀ x1 . x1 ∈ famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1) ⟶ ∀ x2 : ο . (SNo x1 ⟶ SNoLe 0 x1 ⟶ SNoLt x0 (mul_SNo x1 x1) ⟶ x2) ⟶ x2) ⟶ SNoLe 0 (SNoCut (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1)))

as obj
-

as prop
abe56..^{sqrt_SNo_nonneg_prop1c}

theory
HotG

stx
616f4..

address
TMZiC..^{sqrt_SNo_nonneg_prop1c}