diff --git a/src/Lean/Meta/MatchUtil.lean b/src/Lean/Meta/MatchUtil.lean
index 6e22f2913b..e8dcb817fd 100644
--- a/src/Lean/Meta/MatchUtil.lean
+++ b/src/Lean/Meta/MatchUtil.lean
@@ -25,6 +25,19 @@ def matchEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
 def matchHEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr × Expr)) :=
   matchHelper? e fun e => return Expr.heq? e
 
+/--
+  Return `some (α, lhs, rhs)` if `e` is of the form `@Eq α lhs rhs` or `@HEq α lhs α rhs`
+-/
+def matchEqHEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
+  if let some r ← matchEq? e then
+    return some r
+  else if let some (α, lhs, β, rhs) ← matchHEq? e then
+    if (← isDefEq α β) then
+      return some (α, lhs, rhs)
+    return none
+  else
+    return none
+
 def matchFalse (e : Expr) : MetaM Bool := do
   testHelper e fun e => return e.isConstOf ``False
 
diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean
index 4ff2a5901b..dc048fa301 100644
--- a/src/Lean/Meta/Tactic/Injection.lean
+++ b/src/Lean/Meta/Tactic/Injection.lean
@@ -119,7 +119,7 @@ where
     | d+1, fvarId :: fvarIds, mvarId => do
       let cont := do
         go (d+1) fvarIds mvarId
-      if let some (_, lhs, rhs) ← matchEq? (← getLocalDecl fvarId).type then
+      if let some (_, lhs, rhs) ← matchEqHEq? (← getLocalDecl fvarId).type then
         let lhs ← whnf lhs
         let rhs ← whnf rhs
         if lhs.isNatLit && rhs.isNatLit then cont
diff --git a/tests/lean/run/injectionsIssue.lean b/tests/lean/run/injectionsIssue.lean
new file mode 100644
index 0000000000..49b2795564
--- /dev/null
+++ b/tests/lean/run/injectionsIssue.lean
@@ -0,0 +1,11 @@
+inductive Vector (α : Type u): Nat → Type u where
+| nil : Vector α 0
+| cons (head : α) (tail : Vector α n) : Vector α (n+1)
+
+namespace Vector
+
+def nth : Vector α n → Fin n → α
+  | cons x xs, ⟨0, _⟩ => x
+  | cons x xs, ⟨k+1, h⟩ => xs.nth ⟨k, Nat.le_of_succ_le_succ h⟩
+
+attribute [simp] nth