diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index a2f575b273..eaa3de81ca 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -704,7 +704,7 @@ where
         visitQuotLift e
       else if declName == ``Quot.mk then
         visitCtor 3 e
-      else if declName == ``Eq.casesOn || declName == ``Eq.rec || declName == ``Eq.ndrec then
+      else if declName == ``Eq.casesOn || declName == ``Eq.rec || declName == ``Eq.recOn || declName == ``Eq.ndrec then
         visitEqRec e
       else if declName == ``HEq.casesOn || declName == ``HEq.rec || declName == ``HEq.ndrec then
         visitHEqRec e
diff --git a/tests/lean/run/eqRecursors.lean b/tests/lean/run/eqRecursors.lean
new file mode 100644
index 0000000000..19db4ab30f
--- /dev/null
+++ b/tests/lean/run/eqRecursors.lean
@@ -0,0 +1,4 @@
+def castRec {α : Type u} {m n : Nat} (h : m = n) (v : Vector α m) : Vector α n := Eq.rec v h
+def castNdrec {α : Type u} {m n : Nat} (h : m = n) (v : Vector α m) : Vector α n := Eq.ndrec v h
+def castRecOn {α : Type u} {m n : Nat} (h : m = n) (v : Vector α m) : Vector α n := Eq.recOn h v
+def castCasesOn {α : Type u} {m n : Nat} (h : m = n) (v : Vector α m) : Vector α n := Eq.casesOn h v