An exact proof term for the current goal is nat_primrec_S ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x}) (λk p ⇒ (p 0 ∪ SNo_sqrtauxset (p 0) (p 1) x,p 1 ∪ SNo_sqrtauxset (p 0) (p 0) x ∪ SNo_sqrtauxset (p 1) (p 1) x)) n Hn.