Proofgold Term Root Disambiguation

λ x0 x1 x2 . famunion x0 (λ x3 . {div_SNo (add_SNo x2 (mul_SNo x3 x4)) (add_SNo x3 x4)|x4 ∈ x1,SNoLt 0 (add_SNo x3 x4)})

as obj
3fc62..^{SNo_sqrtauxset}

as prop
-

theory
HotG

stx
87341..

address
TMYnp..^{SNo_sqrtauxset}