no goals
f : ℕ → ℕ
m : ℕ
hf : Nat.Primrec f
n : ℕ
⊢ unpaired (fun z n => Nat.rec m (fun y IH => f (unpair (Nat.pair z (Nat.pair y IH))).snd) n) (Nat.pair 0 (id n)) =
    Nat.rec m (fun y IH => f (Nat.pair y IH)) n
simp