Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ or (x0 = 0) (SNoLt 0 (mul_SNo x0 x0))

as obj
-

as prop
48968..^{SNo_zero_or_sqr_pos}

theory
HotG

stx
93147..

address
TMJUp..^{SNo_zero_or_sqr_pos}