diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp
index 1ee38b21ab..828eb8d84d 100644
--- a/src/library/tactic/cases_tactic.cpp
+++ b/src/library/tactic/cases_tactic.cpp
@@ -324,7 +324,11 @@ struct cases_tactic_fn {
             lean_cases_trace(mvar, tout() << "converted heq => eq\n";);
             return unify_eqs(mvar2, num_eqs, updating, new_intros, subst);
         } else if (is_eq(H_type, A, lhs, rhs)) {
-            if (is_local(rhs) || is_local(lhs)) {
+            if (ctx.is_def_eq(lhs, rhs)) {
+                lean_cases_trace(mvar, tout() << "skip\n";);
+                expr mvar2 = clear(m_mctx, *mvar1, H);
+                return unify_eqs(mvar2, num_eqs - 1, updating, new_intros, subst);
+            } else if (is_local(rhs) || is_local(lhs)) {
                 lean_cases_trace(mvar, tout() << "substitute\n";);
                 hsubstitution extra_subst;
                 bool symm  = !is_local(lhs) && is_local(rhs);
diff --git a/tests/lean/run/cases_bug3.lean b/tests/lean/run/cases_bug3.lean
new file mode 100644
index 0000000000..f4bfd428b5
--- /dev/null
+++ b/tests/lean/run/cases_bug3.lean
@@ -0,0 +1,4 @@
+set_option new_elaborator true
+
+theorem ex {A : Type} : ∀ {a a' : A}, a == a' → a = a'
+| a .a (heq.refl .a) := eq.refl a