An exact proof term for the current goal is nat_primrec_S ({0},0) (λk p ⇒ (p 0 ∪ SNo_recipauxset (p 0) x (SNoR x) g ∪ SNo_recipauxset (p 1) x (SNoL_pos x) g,p 1 ∪ SNo_recipauxset (p 0) x (SNoL_pos x) g ∪ SNo_recipauxset (p 1) x (SNoR x) g)) n Hn.