diff --git a/library/init/core.lean b/library/init/core.lean
index fb60948d17..3dba49ef17 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -343,14 +343,9 @@ def std.priority.max     : num := 4294967295
 namespace nat
   protected def prio := num.add std.priority.default 100
 
-  protected def add (a b : nat) : nat :=
-  nat.rec a (λ b₁ r, nat.succ r) b
-
-/- TODO(Leo): use the following definition as soon as we use rfl lemmas for unification
   protected def add : nat → nat → nat
   | a  zero     := a
   | a  (succ b) := succ (add a b)
--/
 
   def of_pos_num : pos_num → nat
   | pos_num.one      := succ zero
diff --git a/tests/lean/671.lean.expected.out b/tests/lean/671.lean.expected.out
index 54dd418b6a..b3c340351c 100644
--- a/tests/lean/671.lean.expected.out
+++ b/tests/lean/671.lean.expected.out
@@ -1,2 +1,2 @@
 protected definition nat.add : ℕ → ℕ → ℕ :=
-λ (a b : ℕ), nat.rec a (λ (b₁ r : ℕ), nat.succ r) b
+nat.add._main
diff --git a/tests/lean/def_inaccessible_issue.lean b/tests/lean/def_inaccessible_issue.lean
index 7cb1aeccab..8d01315540 100644
--- a/tests/lean/def_inaccessible_issue.lean
+++ b/tests/lean/def_inaccessible_issue.lean
@@ -4,7 +4,7 @@ set_option pp.binder_types true
 
 inductive bv : nat → Type
 | nil  : bv 0
-| cons : ∀ (n) (hd : bool) (tl : bv n), bv (succ n)
+| cons : ∀ (n) (hd : bool) (tl : bv n), bv (n+1)
 
 open bv
 
@@ -14,12 +14,4 @@ definition map2 : ∀ {n}, bv n → bv n → bv n
 | 0     nil            nil             := nil
 | (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
 
-check map2._main.equations.eqn_2
-
-/- defining function again without simplifying the type of automatically generated lemmas -/
-
-definition map2' : ∀ {n}, bv n → bv n → bv n
-| 0     nil            nil             := nil
-| (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2' v1 v2)
-
-check map2'._main.equations.eqn_2
+check map2.equations.eqn_2
diff --git a/tests/lean/def_inaccessible_issue.lean.expected.out b/tests/lean/def_inaccessible_issue.lean.expected.out
index fda8389295..e08ab8c4b6 100644
--- a/tests/lean/def_inaccessible_issue.lean.expected.out
+++ b/tests/lean/def_inaccessible_issue.lean.expected.out
@@ -1,10 +1,3 @@
-map2._main.equations.eqn_2 :
-  ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)) (b2 : bool)
-  (v2 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)),
-    map2._main f (cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b1 v1)
-      (cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b2 v2) = cons n (f b1 b2) (map2._main f v1 v2)
-map2'._main.equations.eqn_2 :
-  ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)) (b2 : bool)
-  (v2 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)),
-    map2'._main f (cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b1 v1)
-      (cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b2 v2) = cons n (f b1 b2) (map2'._main f v1 v2)
+map2.equations.eqn_2 :
+  ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n),
+    map2 f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2 f v1 v2)
diff --git a/tests/lean/unfold_crash.lean.expected.out b/tests/lean/unfold_crash.lean.expected.out
index 2e48796691..6cb3ed3e76 100644
--- a/tests/lean/unfold_crash.lean.expected.out
+++ b/tests/lean/unfold_crash.lean.expected.out
@@ -1,3 +1,3 @@
 a b : ℕ,
 H : a = succ b
-⊢ a = succ b
+⊢ a = add._main b 1
diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out
index 78ee85448c..a4a924faf4 100644
--- a/tests/lean/whnf.lean.expected.out
+++ b/tests/lean/whnf.lean.expected.out
@@ -1,4 +1,32 @@
-succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) 0)
+succ
+  (prod.fst
+     (prod.fst
+        (nat.rec
+          (λ (a : ℕ),
+            nat.cases_on 0 (λ (_F : nat.below 0), a)
+              (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
+              poly_unit.star, poly_unit.star)
+          (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
+             (λ (a_1 : ℕ),
+               nat.cases_on (succ a) (λ (_F : nat.below 0), a_1)
+                 (λ (a : ℕ) (_F : nat.below (succ a)), succ (prod.fst (prod.fst _F) a_1))
+                 (ih_1, poly_unit.star), ih_1, poly_unit.star))
+          0, poly_unit.star))
+     2)
 3
-succ (nat.rec a (λ (b₁ r : ℕ), succ r) 0)
+succ
+  (prod.fst
+     (prod.fst
+        (nat.rec
+          (λ (a : ℕ),
+            nat.cases_on 0 (λ (_F : nat.below 0), a)
+              (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
+              poly_unit.star, poly_unit.star)
+          (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
+             (λ (a_1 : ℕ),
+               nat.cases_on (succ a) (λ (_F : nat.below 0), a_1)
+                 (λ (a : ℕ) (_F : nat.below (succ a)), succ (prod.fst (prod.fst _F) a_1))
+                 (ih_1, poly_unit.star), ih_1, poly_unit.star))
+          0, poly_unit.star))
+     a)
 succ a
diff --git a/tests/lean/whnf_cache_bug.lean.expected.out b/tests/lean/whnf_cache_bug.lean.expected.out
index ea56d2351a..dcea7006b6 100644
--- a/tests/lean/whnf_cache_bug.lean.expected.out
+++ b/tests/lean/whnf_cache_bug.lean.expected.out
@@ -1,2 +1,16 @@
 ?m_1
-nat.succ (nat.rec 1 (λ (b₁ r : ℕ), nat.succ r) 0)
+nat.succ
+  (prod.fst
+     (prod.fst
+        (nat.rec
+          (λ (a : ℕ),
+            nat.cases_on 0 (λ (_F : nat.below 0), a)
+              (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
+              poly_unit.star, poly_unit.star)
+          (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
+             (λ (a_1 : ℕ),
+               nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
+                 (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
+                 (ih_1, poly_unit.star), ih_1, poly_unit.star))
+          0, poly_unit.star))
+     1)
diff --git a/tests/lean/whnf_core1.lean.expected.out b/tests/lean/whnf_core1.lean.expected.out
index d9d7f1cdba..95ae6e5c04 100644
--- a/tests/lean/whnf_core1.lean.expected.out
+++ b/tests/lean/whnf_core1.lean.expected.out
@@ -1,4 +1,58 @@
-nat.succ (nat.rec a (λ (b₁ r : ℕ), nat.succ r) (nat.rec 1 (λ (b₁ r : ℕ), nat.succ r) 0))
-nat.succ (nat.rec a (λ (b₁ r : ℕ), nat.succ r) (nat.rec 1 (λ (b₁ r : ℕ), nat.succ r) 0))
+nat.succ
+  (prod.fst
+     (prod.fst
+        (nat.rec
+          (λ (a : ℕ),
+            nat.cases_on 0 (λ (_F : nat.below 0), a)
+              (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
+              poly_unit.star, poly_unit.star)
+          (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
+             (λ (a_1 : ℕ),
+               nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
+                 (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
+                 (ih_1, poly_unit.star), ih_1, poly_unit.star))
+          (prod.fst
+             (prod.fst
+                (nat.rec
+                  (λ (a : ℕ),
+                    nat.cases_on 0 (λ (_F : nat.below 0), a)
+                      (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
+                      poly_unit.star, poly_unit.star)
+                  (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
+                     (λ (a_1 : ℕ),
+                       nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
+                         (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
+                         (ih_1, poly_unit.star), ih_1, poly_unit.star))
+                  0, poly_unit.star))
+             1), poly_unit.star))
+     a)
+nat.succ
+  (prod.fst
+     (prod.fst
+        (nat.rec
+          (λ (a : ℕ),
+            nat.cases_on 0 (λ (_F : nat.below 0), a)
+              (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
+              poly_unit.star, poly_unit.star)
+          (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
+             (λ (a_1 : ℕ),
+               nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
+                 (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
+                 (ih_1, poly_unit.star), ih_1, poly_unit.star))
+          (prod.fst
+             (prod.fst
+                (nat.rec
+                  (λ (a : ℕ),
+                    nat.cases_on 0 (λ (_F : nat.below 0), a)
+                      (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
+                      poly_unit.star, poly_unit.star)
+                  (λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
+                     (λ (a_1 : ℕ),
+                       nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
+                         (λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
+                         (ih_1, poly_unit.star), ih_1, poly_unit.star))
+                  0, poly_unit.star))
+             1), poly_unit.star))
+     a)
 f a
 a + 2