no goals
f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
n : ℕ
⊢ unpaired
      (fun z n =>
        Nat.rec (f z)
          (fun y IH =>
            g
              (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).fst
                (unpair (unpair (Nat.pair z (Nat.pair y IH))).snd).fst))
          n)
      n =
    unpaired (fun z n => Nat.casesOn n (f z) fun y => g (Nat.pair z y)) n
simp