Proofgold Term Root Disambiguation

∀ x0 x1 x2 . x0 ⊆ Sep real (SNoLe 0) ⟶ x1 ⊆ Sep real (SNoLe 0) ⟶ x2 ∈ real ⟶ SNoLe 0 x2 ⟶ SNo_sqrtauxset x0 x1 x2 ⊆ Sep real (SNoLe 0)

as obj
-

as prop
3226b..^{SNo_sqrtauxset_real_nonneg}

theory
HotG

stx
be867..

address
TMbcM..^{SNo_sqrtauxset_real_nonneg}