Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ sqrt_SNo_nonneg x0 = SNoCut (famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 0)) (famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1))

as obj
-

as prop
edc75..^{sqrt_SNo_nonneg_eq}

theory
HotG

stx
87341..

address
TMEsC..^{sqrt_SNo_nonneg_eq}