no goals
n : ℕ
f g : Vector ℕ n → ℕ
h : Vector ℕ (n + 2) → ℕ
hf : Primrec' f
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v => Nat.rec (g v) (fun y IH => h (y ::ᵥ IH ::ᵥ v)) (f v)
simpa using comp' (prec hg hh) (hf.cons idv)