diff --git a/library/init/core.lean b/library/init/core.lean
index 112d03b562..8de48b5414 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -155,6 +155,14 @@ prefix `¬` := not
 inductive eq {α : Sort u} (a : α) : α → Prop
 | refl : eq a
 
+@[elab_as_eliminator, inline, reducible]
+def {u1 u2} eq.ndrec {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : eq a b) : C b :=
+@eq.rec α a (λ α _, C α) m b h
+
+@[elab_as_eliminator, inline, reducible]
+def {u1 u2} eq.ndrec_on {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : eq a b) (m : C a) : C b :=
+@eq.rec α a (λ α _, C α) m b h
+
 /-
 Initialize the quotient module, which effectively adds the following definitions:
 
@@ -201,7 +209,7 @@ attribute [refl] eq.refl
 
 @[elab_as_eliminator, subst]
 theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
-eq.rec h₂ h₁
+eq.ndrec h₂ h₁
 
 notation h1 ▸ h2 := eq.subst h1 h2
 
@@ -218,7 +226,7 @@ infix == := heq
 theorem eq_of_heq {α : Sort u} {a a' : α} (h : a == a') : a = a' :=
 have ∀ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from
   λ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl),
-show (eq.rec_on (eq.refl α) a : α) = a', from
+show (eq.ndrec_on (eq.refl α) a : α) = a', from
   this α a' h (eq.refl α)
 
 /- The following four lemmas could not be automatically generated when the
@@ -616,8 +624,11 @@ assume hp, h₂ (h₁ hp)
 
 def trivial : true := ⟨⟩
 
+@[inline] def false.elim {C : Sort u} (h : false) : C :=
+false.rec (λ _, C) h
+
 @[inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
-false.rec b (h₂ h₁)
+false.elim (h₂ h₁)
 
 theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha)
 
@@ -625,9 +636,6 @@ theorem not.intro {a : Prop} (h : a → false) : ¬ a := h
 
 theorem not_false : ¬false := id
 
-@[inline] def false.elim {C : Sort u} (h : false) : C :=
-false.rec C h
-
 -- proof irrelevance is built in
 theorem proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
 
@@ -706,14 +714,22 @@ attribute [refl] heq.refl
 section
 variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
 
+@[elab_as_eliminator]
+theorem {u1 u2} heq.ndrec {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a == b) : C b :=
+@heq.rec α a (λ β b _, C b) m β b h
+
+@[elab_as_eliminator]
+theorem {u1 u2} heq.ndrec_on {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a == b) (m : C a) : C b :=
+@heq.rec α a (λ β b _, C b) m β b h
+
 theorem heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a == b) (h₂ : p a) : p b :=
 eq.rec_on (eq_of_heq h₁) h₂
 
 theorem heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a == b) (h₂ : p α a) : p β b :=
-heq.rec_on h₁ h₂
+heq.ndrec_on h₁ h₂
 
 @[symm] theorem heq.symm (h : a == b) : b == a :=
-heq.rec_on h (heq.refl a)
+heq.ndrec_on h (heq.refl a)
 
 theorem heq_of_eq (h : a = a') : a == a' :=
 eq.subst h (heq.refl a)
@@ -728,7 +744,7 @@ heq.trans h₁ (heq_of_eq h₂)
 heq.trans (heq_of_eq h₁) h₂
 
 def type_eq_of_heq (h : a == b) : α = β :=
-heq.rec_on h (eq.refl α)
+heq.ndrec_on h (eq.refl α)
 end
 
 theorem eq_rec_heq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p
@@ -745,9 +761,6 @@ theorem heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α}
 theorem of_heq_true {a : Prop} (h : a == true) : a :=
 of_eq_true (eq_of_heq h)
 
-theorem eq_rec_compose : ∀ {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a
-| α _ _ rfl rfl a := rfl
-
 theorem cast_heq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a == a
 | α _ rfl a := heq.refl a
 
@@ -772,7 +785,8 @@ assume not_em : ¬(a ∨ ¬a),
 
 def not_not_em := non_contradictory_em
 
-theorem or.swap : a ∨ b → b ∨ a := or.rec or.inr or.inl
+theorem or.swap (h : a ∨ b) : b ∨ a :=
+or.elim h or.inr or.inl
 
 def or.symm := @or.swap
 
@@ -780,7 +794,8 @@ def or.symm := @or.swap
 def xor (a b : Prop) := (a ∧ ¬ b) ∨ (b ∧ ¬ a)
 
 @[recursor 5]
-theorem iff.elim : ((a → b) → (b → a) → c) → (a ↔ b) → c := iff.rec
+theorem iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
+iff.rec h₁ h₂
 
 theorem iff.elim_left : (a ↔ b) → a → b := iff.mp
 
@@ -833,7 +848,7 @@ iff.intro
   (λ hr, h)
 
 theorem iff_false_intro (h : ¬a) : a ↔ false :=
-iff.intro h (false.rec a)
+iff.intro h (false.rec (λ _, a))
 
 theorem imp_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) :=
 iff.intro
@@ -971,13 +986,13 @@ iff_true_intro (or.inr trivial)
 iff_true_intro (or.inl trivial)
 
 @[simp] theorem or_false (a : Prop) : a ∨ false ↔ a :=
-iff.intro (or.rec id false.elim) or.inl
+iff.intro (λ h, or.elim h id false.elim) or.inl
 
 @[simp] theorem false_or (a : Prop) : false ∨ a ↔ a :=
 iff.trans or_comm (or_false a)
 
 @[simp] theorem or_self (a : Prop) : a ∨ a ↔ a :=
-iff.intro (or.rec id id) or.inl
+iff.intro (λ h, or.elim h id id) or.inl
 
 theorem not_or {a b : Prop} : ¬ a → ¬ b → ¬ (a ∨ b)
 | hna hnb (or.inl ha) := absurd ha hna
@@ -1185,7 +1200,7 @@ else is_false (assume h : p ∧ q, hp (and.left h))
 instance [decidable p] [decidable q] : decidable (p ∨ q) :=
 if hp : p then is_true (or.inl hp) else
   if hq : q then is_true (or.inr hq) else
-    is_false (or.rec hp hq)
+    is_false (λ h, or.elim h hp hq)
 
 instance [decidable p] : decidable (¬p) :=
 if hp : p then is_false (absurd hp) else is_true hp
@@ -1206,11 +1221,11 @@ else
 
 instance [decidable p] [decidable q] : decidable (xor p q) :=
 if hp : p then
-  if hq : q then is_false (or.rec (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p)))
+  if hq : q then is_false (λ h, or.elim h (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p)))
   else is_true $ or.inl ⟨hp, hq⟩
 else
   if hq : q then is_true $ or.inr ⟨hq, hp⟩
-  else is_false (or.rec (λ ⟨h, _⟩, hp h : ¬(p ∧ ¬ q)) (λ ⟨h, _⟩, hq h : ¬(q ∧ ¬ p)))
+  else is_false (λ h, or.elim h (λ ⟨h, _⟩, hp h : ¬(p ∧ ¬ q)) (λ ⟨h, _⟩, hq h : ¬(q ∧ ¬ p)))
 
 instance exists_prop_decidable {p} (P : p → Prop) [decidable p] [s : ∀ h, decidable (P h)] : decidable (∃ h, P h) :=
 if h : p then decidable_of_decidable_of_iff (s h)
@@ -1240,7 +1255,7 @@ instance : decidable_eq bool
 def decidable_eq_of_bool_pred {α : Sort u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α :=
 assume x y : α,
  if hp : p x y = tt then is_true (h₁ hp)
- else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z, ¬p z y = tt) _ hxy hp))
+ else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z _, ¬p z y = tt) _ hxy hp))
 
 theorem decidable_eq_inl_refl {α : Sort u} [h : decidable_eq α] (a : α) : h a a = is_true (eq.refl a) :=
 match (h a a) with
@@ -1272,10 +1287,10 @@ match h with
 | (is_false hnc) := rfl
 
 theorem implies_of_if_pos {c t e : Prop} [decidable c] (h : ite c t e) : c → t :=
-assume hc, eq.rec_on (if_pos hc : ite c t e = t) h
+assume hc, eq.ndrec_on (if_pos hc : ite c t e = t) h
 
 theorem implies_of_if_neg {c t e : Prop} [decidable c] (h : ite c t e) : ¬c → e :=
-assume hnc, eq.rec_on (if_neg hnc : ite c t e = e) h
+assume hnc, eq.ndrec_on (if_neg hnc : ite c t e = e) h
 
 theorem if_ctx_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
                    {x y u v : α}
@@ -1495,11 +1510,11 @@ match h with
 /- Equalities for rewriting let-expressions -/
 theorem let_value_eq {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β) :
                    a₁ = a₂ → (let x : α := a₁ in b x) = (let x : α := a₂ in b x) :=
-λ h, eq.rec_on h rfl
+λ h, eq.ndrec_on h rfl
 
 theorem let_value_heq {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : Π x : α, β x) :
                     a₁ = a₂ → (let x : α := a₁ in b x) == (let x : α := a₂ in b x) :=
-λ h, eq.rec_on h (heq.refl (b a₁))
+λ h, eq.ndrec_on h (heq.refl (b a₁))
 
 theorem let_body_eq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : Π x : α, β x} :
                   (∀ x, b₁ x = b₂ x) → (let x : α := a in b₁ x) = (let x : α := a in b₂ x) :=
@@ -1507,7 +1522,7 @@ theorem let_body_eq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : Π
 
 theorem let_eq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β} :
              a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : α := a₁ in b₁ x) = (let x : α := a₂ in b₂ x) :=
-λ h₁ h₂, eq.rec_on h₁ (h₂ a₁)
+λ h₁ h₂, eq.ndrec_on h₁ (h₂ a₁)
 
 section relation
 variables {α : Sort u} {β : Sort v} (r : β → β → Prop)
@@ -1546,6 +1561,22 @@ theorem inv_image.irreflexive (f : α → β) (h : irreflexive r) : irreflexive
 inductive tc {α : Sort u} (r : α → α → Prop) : α → α → Prop
 | base  : ∀ a b, r a b → tc a b
 | trans : ∀ a b c, tc a b → tc b c → tc a c
+
+@[elab_as_eliminator]
+theorem {u1 u2} tc.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
+                (m₁ : ∀ (a b : α), r a b → C a b)
+                (m₂ : ∀ (a b c : α), tc r a b → tc r b c → C a b → C b c → C a c)
+                {a b : α} (h : tc r a b) : C a b :=
+@tc.rec α r (λ a b _, C a b) m₁ m₂ a b h
+
+@[elab_as_eliminator]
+theorem {u1 u2} tc.ndrec_on {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
+                {a b : α} (h : tc r a b)
+                (m₁ : ∀ (a b : α), r a b → C a b)
+                (m₂ : ∀ (a b c : α), tc r a b → tc r b c → C a b → C b c → C a c)
+                : C a b :=
+@tc.rec α r (λ a b _, C a b) m₁ m₂ a b h
+
 end relation
 
 section binary
@@ -1822,7 +1853,7 @@ quot.ind (λ (a : α), eq.refl (quot.indep f a).1) q
 protected def rec
    (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
    (q : quot r) : β q :=
-eq.rec_on (quot.lift_indep_pr1 f h q) ((lift (quot.indep f) (quot.indep_coherent f h) q).2)
+eq.ndrec_on (quot.lift_indep_pr1 f h q) ((lift (quot.indep f) (quot.indep_coherent f h) q).2)
 
 @[reducible, elab_as_eliminator]
 protected def rec_on
@@ -1965,7 +1996,7 @@ private theorem rel.refl : ∀ q : quotient s, q ~ q :=
 λ q, quot.induction_on q (λ a, setoid.refl a)
 
 private theorem eq_imp_rel {q₁ q₂ : quotient s} : q₁ = q₂ → q₁ ~ q₂ :=
-assume h, eq.rec_on h (rel.refl q₁)
+assume h, eq.ndrec_on h (rel.refl q₁)
 
 theorem exact {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
 assume h, eq_imp_rel h
diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean
index eae4ad12ab..dfffbf5f05 100644
--- a/library/init/data/nat/basic.lean
+++ b/library/init/data/nat/basic.lean
@@ -14,6 +14,14 @@ inductive less_than_or_equal (a : nat) : nat → Prop
 | refl : less_than_or_equal a
 | step : Π {b}, less_than_or_equal b → less_than_or_equal (succ b)
 
+@[elab_as_eliminator]
+theorem less_than_or_equal.ndrec  {a : nat} {C : nat → Prop} (m₁ : C a) (m₂ : ∀ (b : nat), less_than_or_equal a b → C b → C (succ b)) {b : ℕ} (h : less_than_or_equal a b) : C b :=
+@less_than_or_equal.rec a (λ b _, C b) m₁ m₂ b h
+
+@[elab_as_eliminator]
+theorem less_than_or_equal.ndrec_on {a : nat} {C : nat → Prop} {b : ℕ} (h : less_than_or_equal a b) (m₁ : C a) (m₂ : ∀ (b : nat), less_than_or_equal a b → C b → C (succ b)) : C b :=
+@less_than_or_equal.rec a (λ b _, C b) m₁ m₂ b h
+
 instance : has_le nat :=
 ⟨nat.less_than_or_equal⟩
 
@@ -183,7 +191,7 @@ theorem le_succ (n : nat) : n ≤ succ n :=
 less_than_or_equal.step (nat.le_refl n)
 
 theorem succ_le_succ {n m : nat} : n ≤ m → succ n ≤ succ m :=
-λ h, less_than_or_equal.rec (nat.le_refl (succ n)) (λ a b, less_than_or_equal.step) h
+λ h, less_than_or_equal.ndrec (nat.le_refl (succ n)) (λ a b, less_than_or_equal.step) h
 
 theorem succ_lt_succ {n m : nat} : n < m → succ n < succ m :=
 succ_le_succ
@@ -204,7 +212,7 @@ theorem not_lt_zero (n : nat) : ¬ n < 0 :=
 not_succ_le_zero n
 
 theorem pred_le_pred {n m : nat} : n ≤ m → pred n ≤ pred m :=
-λ h, less_than_or_equal.rec_on h
+λ h, less_than_or_equal.ndrec_on h
   (nat.le_refl (pred n))
   (λ n, nat.rec (λ a b, b) (λ a b c, less_than_or_equal.step) n)
 
@@ -243,7 +251,7 @@ protected theorem lt_irrefl (n : nat) : ¬n < n :=
 not_succ_le_self n
 
 protected theorem le_trans {n m k : nat} (h1 : n ≤ m) : m ≤ k → n ≤ k :=
-less_than_or_equal.rec h1 (λ p h2, less_than_or_equal.step)
+less_than_or_equal.ndrec h1 (λ p h2, less_than_or_equal.step)
 
 theorem pred_le : ∀ (n : nat), pred n ≤ n
 | 0        := less_than_or_equal.refl 0
diff --git a/library/init/wf.lean b/library/init/wf.lean
index e119d02fa6..49865d53d4 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -11,6 +11,19 @@ universes u v
 inductive acc {α : Sort u} (r : α → α → Prop) : α → Prop
 | intro (x : α) (h : ∀ y, r y x → acc y) : acc x
 
+@[elab_as_eliminator, inline, reducible]
+def {u1 u2} acc.ndrec {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
+    (m : Π (x : α) (h : ∀ (y : α), r y x → acc r y), (Π (y : α) (a : r y x), C y) → C x)
+    {a : α} (n : acc r a) : C a :=
+@acc.rec α r (λ α _, C α) m a n
+
+@[elab_as_eliminator, inline, reducible]
+def {u1 u2} acc.ndrec_on {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
+    {a : α} (n : acc r a)
+    (m : Π (x : α) (h : ∀ (y : α), r y x → acc r y), (Π (y : α) (a : r y x), C y) → C x)
+    : C a :=
+@acc.rec α r (λ α _, C α) m a n
+
 namespace acc
 variables {α : Sort u} {r : α → α → Prop}
 
@@ -49,7 +62,7 @@ acc.rec_on a (λ x₁ ac₁ ih, F x₁ ih)
 
 theorem fix_F_eq (x : α) (acx : acc r x) :
   fix_F F x acx = F x (λ (y : α) (p : y ≺ x), fix_F F y (acc.inv acx p)) :=
-acc.drec (λ x r ih, rfl) acx
+acc.rec (λ x r ih, rfl) acx
 end
 
 variables {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
@@ -95,8 +108,8 @@ parameters (f : α → β)
 parameters (h : well_founded r)
 
 private def acc_aux {b : β} (ac : acc r b) : ∀ (x : α), f x = b → acc (inv_image r f) x :=
-acc.rec_on ac (λ x acx ih z e,
-  acc.intro z (λ y lt, eq.rec_on e (λ acx ih, ih (f y) lt y rfl) acx ih))
+acc.ndrec_on ac (λ x acx ih z e,
+  acc.intro z (λ y lt, eq.ndrec_on e (λ acx ih, ih (f y) lt y rfl) acx ih))
 
 def accessible {a : α} (ac : acc r (f a)) : acc (inv_image r f) a :=
 acc_aux ac a rfl
@@ -113,9 +126,9 @@ parameters {α : Sort u} {r : α → α → Prop}
 local notation `r⁺` := tc r
 
 def accessible {z : α} (ac : acc r z) : acc (tc r) z :=
-acc.rec_on ac (λ x acx ih,
+acc.ndrec_on ac (λ x acx ih,
   acc.intro x (λ y rel,
-    tc.rec_on rel
+    tc.ndrec_on rel
       (λ a b rab acx ih, ih a rab)
       (λ a b c rab rbc ih₁ ih₂ acx ih, acc.inv (ih₂ acx ih) rab)
       acx ih))
@@ -172,11 +185,11 @@ parameters {ra  : α → α → Prop} {rb  : β → β → Prop}
 local infix `≺`:50 := lex ra rb
 
 def lex_accessible {a} (aca : acc ra a) (acb : ∀ b, acc rb b): ∀ b, acc (lex ra rb) (a, b) :=
-acc.rec_on aca (λ xa aca iha b,
-  acc.rec_on (acb b) (λ xb acb ihb,
+acc.ndrec_on aca (λ xa aca iha b,
+  acc.ndrec_on (acb b) (λ xb acb ihb,
     acc.intro (xa, xb) (λ p lt,
       have aux : xa = xa → xb = xb → acc (lex ra rb) p, from
-        @prod.lex.rec_on α β ra rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁)
+        @prod.lex.rec_on α β ra rb (λ p₁ p₂ _, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁)
                          p (xa, xb) lt
           (λ a₁ b₁ a₂ b₂ h (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), iha a₁ (eq.rec_on eq₂ h) b₁)
           (λ a b₁ b₂ h (eq₂ : a = xa) (eq₃ : b₂ = xb), eq.rec_on eq₂.symm (ihb b₁ (eq.rec_on eq₃ h))),
@@ -188,7 +201,7 @@ def lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra
 
 -- relational product is a subrelation of the lex
 def rprod_sub_lex : ∀ a b, rprod ra rb a b → lex ra rb a b :=
-λ a b h, prod.rprod.rec_on h (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb b₁ b₂ h₁)
+@prod.rprod.rec _ _ ra rb (λ a b _, lex ra rb a b) (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb b₁ b₂ h₁)
 
 -- The relational product of well founded relations is well-founded
 def rprod_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (rprod ra rb) :=
@@ -219,14 +232,14 @@ local infix `≺`:50 := lex r s
 
 def lex_accessible {a} (aca : acc r a) (acb : ∀ a, well_founded (s a))
                      : ∀ (b : β a), acc (lex r s) ⟨a, b⟩ :=
-acc.rec_on aca
+acc.ndrec_on aca
   (λ xa aca (iha : ∀ y, r y xa → ∀ b : β y, acc (lex r s) ⟨y, b⟩),
-    λ b : β xa, acc.rec_on (well_founded.apply (acb xa) b)
+    λ b : β xa, acc.ndrec_on (well_founded.apply (acb xa) b)
       (λ xb acb
         (ihb : ∀ (y : β xa), s xa y xb → acc (lex r s) ⟨xa, y⟩),
         acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩),
           have aux : xa = xa → xb == xb → acc (lex r s) p, from
-            @psigma.lex.rec_on α β r s (λ p₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex r s) p₁)
+            @psigma.lex.rec_on α β r s (λ p₁ p₂ _, p₂.1 = xa → p₂.2 == xb → acc (lex r s) p₁)
                                p ⟨xa, xb⟩ lt
               (λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb),
                 have aux : (∀ (y : α), r y xa → ∀ (b : β y), acc (lex r s) ⟨y, b⟩) →
@@ -286,7 +299,7 @@ acc.rec_on acb
       (λ xa aca (iha : ∀ y, r y xa → acc (rev_lex r s) (mk y xb)),
         acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩),
           have aux : xa = xa → xb = xb → acc (rev_lex r s) p, from
-            @rev_lex.rec_on α β r s (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (rev_lex r s) p₁)
+            @rev_lex.rec_on α β r s (λ p₁ p₂ _, fst p₂ = xa → snd p₂ = xb → acc (rev_lex r s) p₁)
                             p ⟨xa, xb⟩ lt
              (λ a₁ a₂ b (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b = xb),
                show acc (rev_lex r s) ⟨a₁, b⟩, from
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 68ed08e741..046fa760a4 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1137,6 +1137,7 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer<
     trace_elab_debug(tout() << "motive:\n  " << instantiate_mvars(motive) << "\n";);
 
     expr motive_arg = new_args[info.m_motive_idx];
+    trace_elab_debug(tout() << "motive_arg:\n  " << motive_arg << "\n";);
     if (!is_def_eq_all_approx(motive_arg, motive)) {
         throw elaborator_exception(ref, "\"eliminator\" elaborator failed to compute the motive");
     }
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 230f027964..b410e61fe1 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -1176,8 +1176,6 @@ struct structure_cmd_fn {
         name cases_on_name(m_name, "cases_on");
         add_rec_on_alias(cases_on_name);
         m_env = add_aux_recursor(m_env, cases_on_name);
-        if (is_inductive_predicate(m_env, m_name))
-            m_env = mk_drec(m_env, m_name);
     }
 
     // Return the parent names without namespace prefix
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index b3d439d0c3..7b64e51b75 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -518,10 +518,7 @@ struct add_inductive_fn {
 
     /** \brief Initialize m_dep_elim flag. */
     void set_dep_elim() {
-        if (is_zero(m_it_level))
-            m_dep_elim = false;
-        else
-            m_dep_elim = true;
+        m_dep_elim = true;
     }
 
     /** \brief Given t of the form (I As is) where I is the inductive datatypes being defined,
@@ -734,6 +731,7 @@ struct add_inductive_fn {
         declare_intro_rules();
         certified_inductive_decl c = mk_certified_decl(declare_elim_rule());
         m_env = c.add_core(m_env, true);
+        // std::cout << ">> " << m_decl.m_name << " declared\n";
         return mk_pair(m_env, c);
     }
 };
diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index f8c2025ab1..1d1ae50e1d 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -604,7 +604,7 @@ public:
         return ::lean::mk_app({mk_constant(get_heq_trans_name(), {lvl}), A1, B1, B2, a1, b1, b2, H1, H2});
     }
 
-    expr mk_eq_rec(expr const & motive, expr const & H1, expr const & H2) {
+    expr mk_eq_ndrec(expr const & motive, expr const & H1, expr const & H2) {
         if (is_constant(get_app_fn(H2), get_eq_refl_name()))
             return H1;
         expr p       = m_ctx.relaxed_whnf(m_ctx.infer(H2));
@@ -620,11 +620,11 @@ public:
             throw app_builder_exception();
         }
         level l_1    = sort_level(binding_body(mtype));
-        name const & eqrec = get_eq_rec_name();
+        name const & eqrec = get_eq_ndrec_name();
         return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2});
     }
 
-    expr mk_eq_drec(expr const & motive, expr const & H1, expr const & H2) {
+    expr mk_eq_rec(expr const & motive, expr const & H1, expr const & H2) {
         if (is_constant(get_app_fn(H2), get_eq_refl_name()))
             return H1;
         expr p       = m_ctx.relaxed_whnf(m_ctx.infer(H2));
@@ -640,7 +640,7 @@ public:
             throw app_builder_exception();
         }
         level l_1    = sort_level(binding_body(binding_body(mtype)));
-        name const & eqrec = get_eq_drec_name();
+        name const & eqrec = get_eq_rec_name();
         return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2});
     }
 
@@ -856,12 +856,12 @@ expr mk_heq_trans(type_context_old & ctx, expr const & H1, expr const & H2) {
     return app_builder(ctx).mk_heq_trans(H1, H2);
 }
 
-expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2) {
-    return app_builder(ctx).mk_eq_rec(C, H1, H2);
+expr mk_eq_ndrec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2) {
+    return app_builder(ctx).mk_eq_ndrec(C, H1, H2);
 }
 
-expr mk_eq_drec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2) {
-    return app_builder(ctx).mk_eq_drec(C, H1, H2);
+expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2) {
+    return app_builder(ctx).mk_eq_rec(C, H1, H2);
 }
 
 expr mk_eq_of_heq(type_context_old & ctx, expr const & H) {
diff --git a/src/library/app_builder.h b/src/library/app_builder.h
index 070e059f52..9217d4850e 100644
--- a/src/library/app_builder.h
+++ b/src/library/app_builder.h
@@ -113,7 +113,7 @@ expr mk_heq_trans(type_context_old & ctx, expr const & H1, expr const & H2);
     H2 : a = b
     The resultant application is
     @eq.rec A a C H1 b H2 */
-expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2);
+expr mk_eq_ndrec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2);
 
 /** \brief Create a (dependent) eq.drec application.
     C is the motive. The expected types for C, H1 and H2 are
@@ -122,7 +122,7 @@ expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr con
     H2 : a = b
     The resultant application is
     @eq.drec A a C H1 b H2 */
-expr mk_eq_drec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2);
+expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2);
 
 expr mk_eq_of_heq(type_context_old & ctx, expr const & H);
 expr mk_heq_of_eq(type_context_old & ctx, expr const & H);
diff --git a/src/library/congr_lemma.cpp b/src/library/congr_lemma.cpp
index 64153d6900..37956f00cb 100644
--- a/src/library/congr_lemma.cpp
+++ b/src/library/congr_lemma.cpp
@@ -95,9 +95,9 @@ struct congr_lemma_manager {
             }
             expr minor = cast(e, new_type, tail(deps), eqs);
             if (use_drec) {
-                return mk_eq_drec(m_ctx, motive, minor, *major);
-            } else {
                 return mk_eq_rec(m_ctx, motive, minor, *major);
+            } else {
+                return mk_eq_ndrec(m_ctx, motive, minor, *major);
             }
         }
     }
@@ -157,7 +157,7 @@ struct congr_lemma_manager {
             expr x1_refl = mk_eq_refl(m_ctx, x_1);
             new_rhs      = instantiate(abstract(new_rhs, major), x1_refl);
             expr minor   = mk_congr_proof(i+1, lhs, new_rhs, eqs);
-            return mk_eq_drec(m_ctx, motive, minor, major);
+            return mk_eq_rec(m_ctx, motive, minor, major);
         }
     }
 
@@ -500,7 +500,7 @@ struct congr_lemma_manager {
             if (is_heq(m_ctx.infer(eq_pr)))
                 major  = mk_eq_of_heq(m_ctx, eq_pr);
             motive      = m_ctx.mk_lambda({b}, motive);
-            return m_ctx.mk_lambda({a, b, eq_pr}, mk_eq_rec(m_ctx, motive, minor, major));
+            return m_ctx.mk_lambda({a, b, eq_pr}, mk_eq_ndrec(m_ctx, motive, minor, major));
         }
     }
 
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 91b1410fb8..0179cf5c87 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -44,10 +44,10 @@ name const * g_empty = nullptr;
 name const * g_Exists = nullptr;
 name const * g_eq = nullptr;
 name const * g_eq_cases_on = nullptr;
-name const * g_eq_drec = nullptr;
+name const * g_eq_rec = nullptr;
 name const * g_eq_mp = nullptr;
 name const * g_eq_mpr = nullptr;
-name const * g_eq_rec = nullptr;
+name const * g_eq_ndrec = nullptr;
 name const * g_eq_refl = nullptr;
 name const * g_eq_subst = nullptr;
 name const * g_eq_symm = nullptr;
@@ -298,10 +298,10 @@ void initialize_constants() {
     g_Exists = new name{"Exists"};
     g_eq = new name{"eq"};
     g_eq_cases_on = new name{"eq", "cases_on"};
-    g_eq_drec = new name{"eq", "drec"};
+    g_eq_rec = new name{"eq", "rec"};
     g_eq_mp = new name{"eq", "mp"};
     g_eq_mpr = new name{"eq", "mpr"};
-    g_eq_rec = new name{"eq", "rec"};
+    g_eq_ndrec = new name{"eq", "ndrec"};
     g_eq_refl = new name{"eq", "refl"};
     g_eq_subst = new name{"eq", "subst"};
     g_eq_symm = new name{"eq", "symm"};
@@ -553,10 +553,10 @@ void finalize_constants() {
     delete g_Exists;
     delete g_eq;
     delete g_eq_cases_on;
-    delete g_eq_drec;
+    delete g_eq_rec;
     delete g_eq_mp;
     delete g_eq_mpr;
-    delete g_eq_rec;
+    delete g_eq_ndrec;
     delete g_eq_refl;
     delete g_eq_subst;
     delete g_eq_symm;
@@ -807,10 +807,10 @@ name const & get_empty_name() { return *g_empty; }
 name const & get_Exists_name() { return *g_Exists; }
 name const & get_eq_name() { return *g_eq; }
 name const & get_eq_cases_on_name() { return *g_eq_cases_on; }
-name const & get_eq_drec_name() { return *g_eq_drec; }
+name const & get_eq_rec_name() { return *g_eq_rec; }
 name const & get_eq_mp_name() { return *g_eq_mp; }
 name const & get_eq_mpr_name() { return *g_eq_mpr; }
-name const & get_eq_rec_name() { return *g_eq_rec; }
+name const & get_eq_ndrec_name() { return *g_eq_ndrec; }
 name const & get_eq_refl_name() { return *g_eq_refl; }
 name const & get_eq_subst_name() { return *g_eq_subst; }
 name const & get_eq_symm_name() { return *g_eq_symm; }
diff --git a/src/library/constants.h b/src/library/constants.h
index c812341f1e..a838f8c608 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -46,10 +46,10 @@ name const & get_empty_name();
 name const & get_Exists_name();
 name const & get_eq_name();
 name const & get_eq_cases_on_name();
-name const & get_eq_drec_name();
+name const & get_eq_rec_name();
 name const & get_eq_mp_name();
 name const & get_eq_mpr_name();
-name const & get_eq_rec_name();
+name const & get_eq_ndrec_name();
 name const & get_eq_refl_name();
 name const & get_eq_subst_name();
 name const & get_eq_symm_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index acced321d1..66021d054c 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -39,10 +39,10 @@ empty
 Exists
 eq
 eq.cases_on
-eq.drec
+eq.rec
 eq.mp
 eq.mpr
-eq.rec
+eq.ndrec
 eq.refl
 eq.subst
 eq.symm
diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp
index 5493dfcb66..a40098922a 100644
--- a/src/library/constructions/no_confusion.cpp
+++ b/src/library/constructions/no_confusion.cpp
@@ -215,10 +215,10 @@ environment mk_no_confusion(environment const & env, name const & n) {
     gen = Fun(H11, gen);
     // Now, we use gen to build the final proof using eq.rec
     //
-    //  eq.rec InductiveType v1 (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) gen v2 H12 H12
+    //  eq.ndrec InductiveType v1 (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) gen v2 H12 H12
     //
     level eq_rec_l1 = head(ls);
-    expr eq_rec = mk_app(mk_constant(get_eq_rec_name(), {eq_rec_l1, v_lvl}), v_type, v1);
+    expr eq_rec = mk_app(mk_constant(get_eq_ndrec_name(), {eq_rec_l1, v_lvl}), v_type, v1);
     // create eq_rec type_former
     //    (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a)
     expr a   = mk_local(ngen.next(), "a",   v_type, binder_info());
diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
index a581e93348..0db6c99c75 100644
--- a/src/library/equations_compiler/elim_match.cpp
+++ b/src/library/equations_compiler/elim_match.cpp
@@ -1159,7 +1159,7 @@ struct elim_match_fn {
             expr id_M2         = mk_app(ctx1, get_id_name(), M_2);
             expr eqrec_minor   = mk_app(id_M2, g_x1);
             expr eqrec_major   = mk_app(ctx1, f_g_eq_name, x1);
-            eqrec              = mk_eq_rec(ctx1, eqrec_motive, eqrec_minor, eqrec_major);
+            eqrec              = mk_eq_ndrec(ctx1, eqrec_motive, eqrec_minor, eqrec_major);
         } catch (app_builder_exception &) {
             throw_error("equation compiler failed, when trying to build "
                         "'eq.rec'-application for transport step (use 'set_option trace.eqn_compiler.elim_match true' "
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 728a00e518..bc4c87d985 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -455,7 +455,7 @@ static optional<expr> find_if_neg_hypothesis(type_context_old & ctx, expr const
   @eq.rec
      A
      a
-     (fun x : A, (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a))
+     (fun (x : A) (_ : a = x), (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a))
      (fun H : f a = f a, eq.refl (h a))
      (g (f a))
      (eq.symm (g_f_eq a))
@@ -518,8 +518,10 @@ static optional<expr_pair> prove_eq_rec_invertible_aux(type_context_old & ctx, e
     expr eq_rec2    = mk_app(rec_fn, {B, f_x, C, h_x, f_a, H});
     /* (@eq.rec B (f x) C (h x) (f a) H) = h a */
     expr eq_rec2_eq = mk_eq(ctx, eq_rec2, h_a);
-    /* (fun x : A, (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a)) */
-    expr pr_motive  = ctx.mk_lambda(x, ctx.mk_pi(H, eq_rec2_eq));
+    expr a_eq_x     = mk_eq(ctx, a, x);
+    expr h_a_eq_x   = aux_locals.push_local("_h'", a_eq_x);
+    /* (fun (x : A) (h' : a = x), (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a)) */
+    expr pr_motive  = ctx.mk_lambda(x, ctx.mk_lambda(h_a_eq_x, ctx.mk_pi(H, eq_rec2_eq)));
     expr g_f_eq_a   = mk_app(ctx, g_f_name, a);
     /* (eq.symm (g_f_eq a)) */
     expr pr_major   = mk_eq_symm(ctx, g_f_eq_a);
@@ -564,6 +566,8 @@ static optional<expr_pair> prove_eq_rec_invertible(type_context_old & ctx, expr
         if (optional<expr_pair> g_H = prove_eq_rec_invertible_aux(ctx, f)) {
             expr g, H;
             std::tie(g, H) = *g_H;
+            tout() << "H: " << H << "\n";
+            tout() << ">>>>> " << ctx.infer(H) << "\n";
             for (unsigned i = 6; i < args.size(); i++) {
                 // congr_fun : ∀ {α : Sort u_1} {β : α → Sort u_2} {f g : Π (x : α), β x}, f = g → ∀ (a : α), f a = g a
                 expr f_type = ctx.relaxed_whnf(ctx.infer(f));
diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp
index 16f6350cfc..dbf063eaf4 100644
--- a/src/library/inductive_compiler/basic.cpp
+++ b/src/library/inductive_compiler/basic.cpp
@@ -80,34 +80,39 @@ class add_basic_inductive_decl_fn {
         bool gen_cases_on     = get_inductive_cases_on(m_opts);
         bool gen_no_confusion = get_inductive_no_confusion(m_opts);
 
-        if (is_inductive_predicate(m_env, ind_name))
-            m_env = mk_drec(m_env, ind_name);
+        // if (is_inductive_predicate(m_env, ind_name))
+            // m_env = mk_drec(m_env, ind_name);
 
+        lean_trace(name({"inductive_compiler"}), tout() << ">> generate rec_on\n";);
         if (gen_rec_on)
             m_env = mk_rec_on(m_env, ind_name);
 
         if (has_unit) {
+            lean_trace(name({"inductive_compiler"}), tout() << ">> generate cases_on\n";);
             if (gen_cases_on)
                 m_env = mk_cases_on(m_env, ind_name);
 
             if (gen_cases_on && gen_no_confusion && has_eq && has_heq) {
+                lean_trace(name({"inductive_compiler"}), tout() << ">> generate no_confusion\n";);
                 m_env = mk_no_confusion(m_env, ind_name);
+                lean_trace(name({"inductive_compiler"}), tout() << ">> generate injective\n";);
                 m_env = mk_injective_lemmas(m_env, ind_name);
             }
 
             if (gen_brec_on && has_prod) {
+                lean_trace(name({"inductive_compiler"}), tout() << ">> generate below\n";);
                 m_env = mk_below(m_env, ind_name);
+                lean_trace(name({"inductive_compiler"}), tout() << ">> generate ibelow\n";);
                 m_env = mk_ibelow(m_env, ind_name);
             }
         }
 
         if (gen_brec_on && has_unit && has_prod) {
+            lean_trace(name({"inductive_compiler"}), tout() << ">> generate brec_on\n";);
             m_env = mk_brec_on(m_env, ind_name);
+            lean_trace(name({"inductive_compiler"}), tout() << ">> generate binduction_on\n";);
             m_env = mk_binduction_on(m_env, ind_name);
         }
-
-        // if (!m_is_meta)
-        // m_env = mk_has_sizeof(m_env, ind_name);
     }
 
     void send_to_kernel() {
@@ -151,6 +156,7 @@ environment add_basic_inductive_decl(environment const & env, options const & op
 }
 
 void initialize_inductive_compiler_basic() {
+    register_trace_class(name({"inductive_compiler"}));
     register_trace_class(name({"inductive_compiler", "basic"}));
     register_trace_class(name({"inductive_compiler", "basic", "ind"}));
     register_trace_class(name({"inductive_compiler", "basic", "irs"}));
diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index 07ebc86dc1..ead1c0564c 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -1242,7 +1242,7 @@ class add_nested_inductive_decl_fn {
         expr e = m_tctx.relaxed_whnf(lhs);
         buffer<expr> rec_args;
         expr rec_fn = get_app_args(e, rec_args);
-        if (is_constant(rec_fn, get_eq_rec_name())) {
+        if (is_constant(rec_fn, get_eq_ndrec_name())) {
             lean_assert(rec_args.size() == 6);
             simp_result r_first = force_eq_rec(rec_fn, rec_args);
             simp_result r_rest = force_recursors_core(r_first.get_new());
@@ -1254,7 +1254,7 @@ class add_nested_inductive_decl_fn {
 
     simp_result force_eq_rec(expr const & rec_fn, buffer<expr> const & rec_args) {
         // See comments above prove_eq_rec_invertible(type_context_old & ctx, expr const & e) at equation_compiler/util.cpp.
-        lean_assert(is_constant(rec_fn, get_eq_rec_name()) && rec_args.size() == 6);
+        lean_assert(is_constant(rec_fn, get_eq_ndrec_name()) && rec_args.size() == 6);
         expr B      = rec_args[0];
         expr from   = rec_args[1]; /* (f (g (f a))) */
         expr C      = rec_args[2];
@@ -1300,16 +1300,16 @@ class add_nested_inductive_decl_fn {
         expr f_x_eq_f_a = mk_eq(m_tctx, f_x, f_a);
         expr H          = aux_locals.push_local("_H", f_x_eq_f_a);
         expr h_x        = mk_app(h, x);
-        /* (@eq.rec B (f x) C (h x) (f a) H) */
+        /* (@eq.ndrec B (f x) C (h x) (f a) H) */
         expr eq_rec2    = mk_app(rec_fn, {B, f_x, C, h_x, f_a, H});
-        /* (@eq.rec B (f x) C (h x) (f a) H) = h a */
+        /* (@eq.ndrec B (f x) C (h x) (f a) H) = h a */
         expr eq_rec2_eq = mk_eq(m_tctx, eq_rec2, h_a);
         /* (fun x : A, (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a)) */
         expr pr_motive  = m_tctx.mk_lambda(x, m_tctx.mk_pi(H, eq_rec2_eq));
         expr g_f_eq_a   = mk_app(m_tctx, g_f_name, a);
         /* (eq.symm (g_f_eq a)) */
         expr pr_major   = mk_eq_symm(m_tctx, g_f_eq_a);
-        expr pr         = mk_app(mk_constant(get_eq_rec_name(), {mk_level_zero(), A_lvl}),
+        expr pr         = mk_app(mk_constant(get_eq_ndrec_name(), {mk_level_zero(), A_lvl}),
                                  {A, a, pr_motive, pr_minor, g_f_a, pr_major, major});
         return simp_result(h_a, pr);
     }
@@ -1668,7 +1668,7 @@ class add_nested_inductive_decl_fn {
             assert_type_correct(m_outer.m_env, rest);
             assert_type_correct(m_outer.m_env, equality_proof);
 
-            return mk_eq_rec(m_outer.m_tctx, motive, rest, equality_proof);
+            return mk_eq_ndrec(m_outer.m_tctx, motive, rest, equality_proof);
         }
 
     public:
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 5558083c4b..b45a28ad72 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -95,7 +95,7 @@ static vm_obj rewrite_core(expr h, expr e, rewrite_cfg const & cfg, tactic_state
     } catch (exception & ex) {
         throw nested_exception("rewrite tactic failed, motive is not type correct", std::current_exception());
     }
-    expr prf           = mk_eq_rec(ctx, motive, mk_eq_refl(ctx, e), h);
+    expr prf           = mk_eq_ndrec(ctx, motive, mk_eq_refl(ctx, e), h);
     tactic_state new_s = set_mctx_goals(s, ctx.mctx(), append(cons(head(s.goals()), to_list(new_goals)), tail(s.goals())));
     return tactic::mk_success(mk_vm_pair(to_obj(new_e), mk_vm_pair(to_obj(prf), to_obj(to_list(metas)))), new_s);
 }
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index 77b0bfde91..373dceb3e2 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -170,7 +170,7 @@ expr simplify_core_fn::remove_unnecessary_casts(expr const & e) {
                 buffer<expr> cast_args;
                 expr f_cast = get_app_args(args[i], cast_args);
                 name n_f = const_name(f_cast);
-                if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name()) {
+                if (n_f == get_eq_ndrec_name() || n_f == get_eq_rec_name()) {
                     lean_assert(cast_args.size() == 6);
                     expr major_premise = cast_args[5];
                     expr f_major_premise = get_app_fn(major_premise);
diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp
index 6abfb8e2b3..a3e82fdfc9 100644
--- a/src/library/tactic/subst_tactic.cpp
+++ b/src/library/tactic/subst_tactic.cpp
@@ -95,7 +95,7 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
     expr major   = symm ? H2 : mk_eq_symm(ctx2, H2);
     expr mvar3   = ctx2.mk_metavar_decl(lctx, new_type);
     expr minor   = mvar3;
-    expr new_val = depH2 ? mk_eq_drec(ctx2, motive, minor, major) : mk_eq_rec(ctx2, motive, minor, major);
+    expr new_val = depH2 ? mk_eq_rec(ctx2, motive, minor, major) : mk_eq_ndrec(ctx2, motive, minor, major);
     mctx = ctx2.mctx();
     mctx.assign(*mvar2, new_val);
     expr mvar4   = clear(mctx, mvar3, H2);
diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index fff9f8de1b..c9d0b20fd1 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -102,8 +102,6 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
                              num_args, major_pos, params_pos, indices_pos, produce_motive);
     } else if (is_aux_recursor(env, r) &&
                (strcmp(r.get_string(), "cases_on") == 0 ||
-                strcmp(r.get_string(), "dcases_on") == 0 ||
-                strcmp(r.get_string(), "drec_on") == 0 ||
                 strcmp(r.get_string(), "rec_on") == 0   ||
                 strcmp(r.get_string(), "brec_on") == 0)) {
         name I = r.get_prefix();
diff --git a/src/library/util.cpp b/src/library/util.cpp
index fa05239f0f..9e5972205f 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -720,9 +720,16 @@ expr mk_heq(abstract_type_context & ctx, expr const & lhs, expr const & rhs) {
     return mk_app(mk_constant(get_heq_name(), {lvl}), A, lhs, B, rhs);
 }
 
-bool is_eq_rec_core(expr const & e) {
+bool is_eq_ndrec_core(expr const & e) {
     expr const & fn = get_app_fn(e);
-    return is_constant(fn) && const_name(fn) == get_eq_rec_name();
+    return is_constant(fn) && const_name(fn) == get_eq_ndrec_name();
+}
+
+bool is_eq_ndrec(expr const & e) {
+    expr const & fn = get_app_fn(e);
+    if (!is_constant(fn))
+        return false;
+    return const_name(fn) == get_eq_ndrec_name();
 }
 
 bool is_eq_rec(expr const & e) {
@@ -732,13 +739,6 @@ bool is_eq_rec(expr const & e) {
     return const_name(fn) == get_eq_rec_name();
 }
 
-bool is_eq_drec(expr const & e) {
-    expr const & fn = get_app_fn(e);
-    if (!is_constant(fn))
-        return false;
-    return const_name(fn) == get_eq_drec_name();
-}
-
 bool is_eq(expr const & e) {
     return is_app_of(e, get_eq_name(), 3);
 }
@@ -1066,18 +1066,12 @@ expr mk_bool_tt() { return *g_bool_tt; }
 expr mk_bool_ff() { return *g_bool_ff; }
 expr to_bool_expr(bool b) { return b ? mk_bool_tt() : mk_bool_ff(); }
 
-name get_dep_recursor(environment const & env, name const & n) {
-    if (is_inductive_predicate(env, n))
-        return name(n, "drec");
-    else
-        return name(n, "rec");
+name get_dep_recursor(environment const &, name const & n) {
+    return name(n, "rec");
 }
 
-name get_dep_cases_on(environment const & env, name const & n) {
-    if (is_inductive_predicate(env, n))
-        return name(n, "dcases_on");
-    else
-        return name(n, "cases_on");
+name get_dep_cases_on(environment const &, name const & n) {
+    return name(n, "cases_on");
 }
 
 static char const * g_aux_meta_rec_prefix = "_meta_aux";