Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ real ⟶ SNoLe 0 x0 ⟶ sqrt_SNo_nonneg x0 ∈ real

as obj
-

as prop
51186..^{sqrt_SNo_nonneg_real}

theory
HotG

stx
be867..

address
TMPki..^{sqrt_SNo_nonneg_real}