Proofgold Term Root Disambiguation

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

as obj
-

as prop
85b0b..^{sqrt_SNo_nonneg_SNoS_omega}

theory
HotG

stx
be867..

address
TMY9m..^{sqrt_SNo_nonneg_SNoS_omega}