diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 6f1c3d35ce..2c7dac6471 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -166,12 +166,12 @@ inductive Eq {α : Sort u} (a : α) : α → Prop
 | refl {} : Eq a
 
 @[elabAsEliminator, inline, reducible]
-def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b :=
-@Eq.rec α a (fun α _ => C α) m b h
+def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
+@Eq.rec α a (fun α _ => motive α) m b h
 
 @[elabAsEliminator, inline, reducible]
-def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : Eq a b) (m : C a) : C b :=
-@Eq.rec α a (fun α _ => C α) m b h
+def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) : motive b :=
+@Eq.rec α a (fun α _ => motive α) m b h
 
 /-
 Initialize the Quotient Module, which effectively adds the following definitions:
@@ -744,12 +744,12 @@ section
 variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
 
 @[elabAsEliminator]
-theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
-@HEq.rec α a (fun β b _ => C b) m β b h
+theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : ∀ {β : Sort u2}, β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b :=
+@HEq.rec α a (fun β b _ => motive b) m β b h
 
 @[elabAsEliminator]
-theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
-@HEq.rec α a (fun β b _ => C b) m β b h
+theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : motive a) : motive b :=
+@HEq.rec α a (fun β b _ => motive b) m β b h
 
 theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
 Eq.recOn (eqOfHEq h₁) h₂