diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index f057ee311d..d605f7634c 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -20,7 +20,7 @@ def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
     (symm : Bool := false) (occs : Occurrences := Occurrences.all) (mode := TransparencyMode.reducible) : MetaM RewriteResult :=
   withMVarContext mvarId do
     checkNotAssigned mvarId `rewrite
-    let heqType ← inferType heq
+    let heqType ← instantiateMVars (← inferType heq)
     let (newMVars, binderInfos, heqType) ← forallMetaTelescopeReducing heqType
     let heq := mkAppN heq newMVars
     let cont (heq heqType : Expr) : MetaM RewriteResult := do
diff --git a/tests/lean/run/rw_inst_mvars.lean b/tests/lean/run/rw_inst_mvars.lean
new file mode 100644
index 0000000000..eff45a55f5
--- /dev/null
+++ b/tests/lean/run/rw_inst_mvars.lean
@@ -0,0 +1,6 @@
+example  (p : Nat → Prop) (h : ∀ n, p (n+1) = p n) : (p m ↔ p 0) := by
+  induction m
+  case succ ih =>
+    rw [h, ih]
+    exact Iff.rfl
+  case zero => exact Iff.rfl