diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
index 9e19315028..48856b50f5 100644
--- a/src/library/equations_compiler/elim_match.cpp
+++ b/src/library/equations_compiler/elim_match.cpp
@@ -601,7 +601,7 @@ struct elim_match_fn {
         for (equation const & eqn : P.m_equations) {
             equation new_eqn   = eqn;
             new_eqn.m_patterns = tail(eqn.m_patterns);
-            if (is_var_transition) {
+            if (is_var_transition || is_local(head(eqn.m_patterns))) {
                 new_eqn.m_subst  = add_subst(eqn.m_subst, head(eqn.m_patterns), head(P.m_var_stack));
             }
             new_eqns.push_back(new_eqn);
diff --git a/tests/lean/run/eqn_compiler_variable_or_inaccessible.lean b/tests/lean/run/eqn_compiler_variable_or_inaccessible.lean
new file mode 100644
index 0000000000..87fc7872e6
--- /dev/null
+++ b/tests/lean/run/eqn_compiler_variable_or_inaccessible.lean
@@ -0,0 +1,4 @@
+example {α : Type} {p q : α → Prop} {x : α} (h : ∀ y, p y → q y) (hx : q x) :
+  ∀ y, x = y ∨ p y → q y
+| x  (or.inr p)   := h x p
+| ._ (or.inl rfl) := hx