Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ SNoLe 0 x0 ⟶ sqrt_SNo_nonneg (exp_SNo_nat x0 2) = x0

as obj
-

as prop
21b2d..^{sqrt_SNo_nonneg_sqr_id}

theory
HotG

stx
2ea7a..

address
TMVLr..^{sqrt_SNo_nonneg_sqr_id}