cf cg : Code
a : ℕ
⊢ Nat.rec (eval cf (a, 0).fst)
      (fun y IH => do
        let i ← IH
        eval cg (Nat.pair (a, 0).fst (Nat.pair y i)))
      (a, 0).snd =
    eval cf a
cf cg : Code
a : ℕ
⊢ eval (prec cf cg) (Nat.pair a 0) = eval cf a
rw [eval, Nat.unpaired, Nat.unpair_pair]
cf cg : Code
a : ℕ
⊢ Nat.rec (eval cf a)
      (fun y IH => do
        let i ← IH
        eval cg (Nat.pair a (Nat.pair y i)))
      0 =
    eval cf a
cf cg : Code
a : ℕ
⊢ Nat.rec (eval cf (a, 0).fst)
      (fun y IH => do
        let i ← IH
        eval cg (Nat.pair (a, 0).fst (Nat.pair y i)))
      (a, 0).snd =
    eval cf a
simp (config := { Lean.Meta.Simp.neutralConfig with proj := true }) only []
no goals
cf cg : Code
a : ℕ
⊢ Nat.rec (eval cf a)
      (fun y IH => do
        let i ← IH
        eval cg (Nat.pair a (Nat.pair y i)))
      0 =
    eval cf a
rw [Nat.rec_zero]