diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp
index de67c3e850..5366ab29da 100644
--- a/src/library/tactic/cases_tactic.cpp
+++ b/src/library/tactic/cases_tactic.cpp
@@ -21,43 +21,6 @@ Author: Leonardo de Moura
 #include "library/tactic/subst_tactic.h"
 
 namespace lean {
-expr apply_substitutions(expr const & e, substitutions const & s) {
-    if (s.empty()) return e;
-    if (!has_local(e)) return e;
-    return replace(e, [&](expr const & e, unsigned) {
-            if (!has_local(e)) return some_expr(e);
-            if (is_local(e)) {
-                if (auto r = s.find(mlocal_name(e)))
-                    return some_expr(*r);
-            }
-            return none_expr();
-        });
-}
-
-list<expr> apply_substitutions(list<expr> const & es, substitutions const & s) {
-    if (s.empty()) return es;
-    return map(es, [&](expr const & e) { return apply_substitutions(e, s); });
-}
-
-substitutions apply_substitutions(substitutions const & s1, substitutions const & s2) {
-    if (s2.empty()) return s1;
-    substitutions R;
-    s1.for_each([&](name const & x, expr const & e) {
-            R.insert(x, apply_substitutions(e, s2));
-        });
-    return R;
-}
-
-substitutions merge(substitutions const & s1, substitutions const & s2) {
-    if (s1.empty()) return s2;
-    if (s2.empty()) return s1;
-    substitutions R = s1;
-    s2.for_each([&](name const & x, expr const & e) {
-            R.insert(x, e);
-        });
-    return R;
-}
-
 struct cases_tactic_exception : public exception {
     tactic_state m_state;
     cases_tactic_exception(tactic_state const & s, char const * msg):exception(msg), m_state(s) {}
@@ -410,17 +373,10 @@ struct cases_tactic_fn {
         } else if (is_eq(H_type, A, lhs, rhs)) {
             if (is_local(rhs) || is_local(lhs)) {
                 lean_cases_trace(mvar, tout() << "substitute\n";);
-                name_map<name> extra_renames;
+                substitutions extra_substs;
                 bool symm  = !is_local(lhs) && is_local(rhs);
                 expr mvar2 = subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm,
-                                   updating ? &extra_renames : nullptr);
-                substitutions extra_substs = to_substitutions(mvar2, extra_renames);
-                if (updating) {
-                    if (symm)
-                        extra_substs.insert(mlocal_name(rhs), apply_substitutions(lhs, extra_substs));
-                    else
-                        extra_substs.insert(mlocal_name(lhs), apply_substitutions(rhs, extra_substs));
-                }
+                                   updating ? &extra_substs : nullptr);
                 new_intros = apply_substitutions(new_intros, extra_substs);
                 substs     = merge(apply_substitutions(substs, extra_substs), extra_substs);
                 return unify_eqs(mvar2, num_eqs - 1, updating, new_intros, substs);
diff --git a/src/library/tactic/cases_tactic.h b/src/library/tactic/cases_tactic.h
index 8ef7b90d32..30d214b320 100644
--- a/src/library/tactic/cases_tactic.h
+++ b/src/library/tactic/cases_tactic.h
@@ -6,23 +6,12 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "library/tactic/induction_tactic.h"
+#include "library/tactic/subst_tactic.h"
 
 namespace lean {
 typedef list<list<expr>>    xintros_list;
-typedef name_map<expr>      substitutions;
 typedef list<substitutions> substitutions_list;
 
-/* \brief Given `e`, for each (x := v) in `s` replace `x` with `v` in `e` */
-expr apply_substitutions(expr const & e, substitutions const & s);
-list<expr> apply_substitutions(list<expr> const & es, substitutions const & s);
-
-/* \brief Return a new set of substitutions containing (x := apply_substitutions(v, s2)) for
-   each (x := v) in `s1`. */
-substitutions apply_substitutions(substitutions const & s1, substitutions const & s2);
-
-/* \brief Return a new set of substitutions containing the entries of `s1` and `s2`. */
-substitutions merge(substitutions const & s1, substitutions const & s2);
-
 /** \brief Similar to induction, but applies 'cases_on' and has bettern support for dependent types. Failures are reported using exceptions.
     \c ids (if available) provides the names for new hypotheses.
     If ilist and slist are not nullptr, then
diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp
index 213beaf929..7f5ff22ec6 100644
--- a/src/library/tactic/subst_tactic.cpp
+++ b/src/library/tactic/subst_tactic.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
+#include "kernel/replace_fn.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "library/util.h"
@@ -20,6 +21,43 @@ Author: Leonardo de Moura
 #include "library/tactic/app_builder_tactics.h"
 
 namespace lean {
+expr apply_substitutions(expr const & e, substitutions const & s) {
+    if (s.empty()) return e;
+    if (!has_local(e)) return e;
+    return replace(e, [&](expr const & e, unsigned) {
+            if (!has_local(e)) return some_expr(e);
+            if (is_local(e)) {
+                if (auto r = s.find(mlocal_name(e)))
+                    return some_expr(*r);
+            }
+            return none_expr();
+        });
+}
+
+list<expr> apply_substitutions(list<expr> const & es, substitutions const & s) {
+    if (s.empty()) return es;
+    return map(es, [&](expr const & e) { return apply_substitutions(e, s); });
+}
+
+substitutions apply_substitutions(substitutions const & s1, substitutions const & s2) {
+    if (s2.empty()) return s1;
+    substitutions R;
+    s1.for_each([&](name const & x, expr const & e) {
+            R.insert(x, apply_substitutions(e, s2));
+        });
+    return R;
+}
+
+substitutions merge(substitutions const & s1, substitutions const & s2) {
+    if (s1.empty()) return s2;
+    if (s2.empty()) return s1;
+    substitutions R = s1;
+    s2.for_each([&](name const & x, expr const & e) {
+            R.insert(x, e);
+        });
+    return R;
+}
+
 /* For debugging purposes, make sure H is in the local context for mvar */
 bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar, name const & H) {
     local_context lctx = mctx.get_metavar_decl(mvar)->get_context();
@@ -31,7 +69,7 @@ bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar
 }
 
 expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
-           expr const & mvar, expr const & H, bool symm, name_map<name> * renames) {
+           expr const & mvar, expr const & H, bool symm, substitutions * substs) {
     #define lean_subst_trace(CODE) lean_trace(name({"tactic", "subst"}), CODE)
 #define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S(env, opts, mctx, to_list(MVAR), MVAR); type_context TMP_CTX = mk_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp() << "\n";)
 
@@ -43,6 +81,7 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
     expr lhs, rhs;
     lean_verify(is_eq(H_type, lhs, rhs));
     if (symm) std::swap(lhs, rhs);
+    expr init_lhs = lhs;
     buffer<expr> to_revert;
     to_revert.push_back(lhs);
     to_revert.push_back(H);
@@ -86,14 +125,16 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
     optional<expr> mvar6 = intron(env, opts, mctx, mvar5, to_revert.size() - 2, new_Hnames);
     if (!mvar6) throw exception("subst tactic failed, unexpected failure when re-introducing dependencies");
     lean_assert(new_Hnames.size() == to_revert.size() - 2);
-    if (renames) {
-        name_map<name> rmap;
+    if (substs) {
+        local_context lctx = mctx.get_metavar_decl(*mvar6)->get_context();
+        substitutions new_substs;
         for (unsigned i = 0; i < to_revert.size() - 2; i++) {
             lean_assert(check_hypothesis_in_context(mctx, mvar, mlocal_name(to_revert[i+2])));
             lean_assert(check_hypothesis_in_context(mctx, *mvar6, new_Hnames[i]));
-            rmap.insert(mlocal_name(to_revert[i+2]), new_Hnames[i]);
+            new_substs.insert(mlocal_name(to_revert[i+2]), lctx.get_local_decl(new_Hnames[i])->mk_ref());
         }
-        *renames = rmap;
+        new_substs.insert(mlocal_name(init_lhs), apply_substitutions(rhs, new_substs));
+        *substs = new_substs;
     }
     lean_subst_trace_state(*mvar6, "after intro remaining reverted hypotheses:\n");
     return *mvar6;
diff --git a/src/library/tactic/subst_tactic.h b/src/library/tactic/subst_tactic.h
index f49de6f9ad..1cd0577c50 100644
--- a/src/library/tactic/subst_tactic.h
+++ b/src/library/tactic/subst_tactic.h
@@ -8,9 +8,22 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic_state.h"
 
 namespace lean {
+typedef name_map<expr>      substitutions;
+
+/* \brief Given `e`, for each (x := v) in `s` replace `x` with `v` in `e` */
+expr apply_substitutions(expr const & e, substitutions const & s);
+list<expr> apply_substitutions(list<expr> const & es, substitutions const & s);
+
+/* \brief Return a new set of substitutions containing (x := apply_substitutions(v, s2)) for
+   each (x := v) in `s1`. */
+substitutions apply_substitutions(substitutions const & s1, substitutions const & s2);
+
+/* \brief Return a new set of substitutions containing the entries of `s1` and `s2`. */
+substitutions merge(substitutions const & s1, substitutions const & s2);
+
 /** \brief Given (H : lhs = rhs), replace lhs with rhs in the goal \c mvar. If symm == true, then replace rhs with lhs.
-    The replaced term must be a local constant. If renames is not nullptr, then hypotheses renamed by revert/intro
-    are stored in \c renames.
+    The replaced term must be a local constant. If substs is not nullptr, then hypotheses renamed by revert/intro
+    are stored in \c substs, and the actual substitution.
 
     \pre is_metavar(mvar)
     \pre is_local(H)
@@ -19,7 +32,7 @@ namespace lean {
     \pre symm == false ==> is_local(lhs(typeof(H)))
     \pre symm == false ==> is_local(rhs(typeof(H))) */
 expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
-           expr const & mvar, expr const & H, bool symm, name_map<name> * renames);
+           expr const & mvar, expr const & H, bool symm, substitutions * substs);
 
 void initialize_subst_tactic();
 void finalize_subst_tactic();