no goals
f : ℕ → ℕ → ℕ
hf : Primrec' fun v => f (Vector.head v) (Vector.head (Vector.tail v))
n : ℕ
g h : Vector ℕ n → ℕ
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v => f (g v) (h v)
simpa using hf.comp' (hg.cons <| hh.cons Primrec'.nil)