diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp
index 22d57b86db..e5dcd25e77 100644
--- a/src/library/tactic/subst_tactic.cpp
+++ b/src/library/tactic/subst_tactic.cpp
@@ -19,11 +19,14 @@ Author: Leonardo de Moura
 
 namespace lean {
 static void split_deps(buffer<expr> const & hyps, expr const & x, expr const & h,
-                       buffer<expr> & non_deps, buffer<expr> & deps) {
+                       buffer<expr> & non_deps, buffer<expr> & deps, bool & depends_on_h) {
     for (expr const & hyp : hyps) {
         if (hyp == h || hyp == x) {
             // we clear h and x
-        } else if (depends_on(hyp, x) || depends_on(hyp, h) || depends_on_any(hyp, deps)) {
+        } else if (depends_on(hyp, h)) {
+            deps.push_back(hyp);
+            depends_on_h = true;
+        } else if (depends_on(hyp, x) || depends_on_any(hyp, deps)) {
             deps.push_back(hyp);
         } else {
             non_deps.push_back(hyp);
@@ -52,14 +55,18 @@ tactic mk_subst_tactic_core(name const & h_name, bool symm) {
             return none_proof_state();
         buffer<expr> hyps, deps, non_deps;
         g.get_hyps(hyps);
-        split_deps(hyps, lhs, h, non_deps, deps);
+        bool depends_on_h = depends_on(g.get_type(), h);
+        split_deps(hyps, lhs, h, non_deps, deps, depends_on_h);
         // revert dependencies
         expr type = Pi(deps, g.get_type());
         // substitute
         bool has_dep_elim = inductive::has_dep_elim(env, get_eq_name());
+        bool use_dep_elim = has_dep_elim;
+        if (depends_on_h)
+            use_dep_elim = true;
         expr motive, new_type;
         new_type = instantiate(abstract_local(type, mlocal_name(lhs)), rhs);
-        if (has_dep_elim) {
+        if (use_dep_elim) {
             new_type = instantiate(abstract_local(new_type, mlocal_name(h)), mk_refl(*tc, rhs));
             if (symm) {
                 motive = Fun(lhs, Fun(h, type));
@@ -90,7 +97,6 @@ tactic mk_subst_tactic_core(name const & h_name, bool symm) {
         expr new_meta_core = mk_app(new_metavar, non_deps);
         expr new_meta      = mk_app(new_meta_core, intros_hyps);
         goal new_g(new_meta, new_goal_type);
-
         // create eqrec term
         substitution new_subst = s.get_subst();
         expr major = symm ? h : mk_symm(*tc, h);
@@ -98,8 +104,13 @@ tactic mk_subst_tactic_core(name const & h_name, bool symm) {
         expr A     = tc->infer(lhs).first;
         level l1   = sort_level(tc->ensure_type(new_type).first);
         level l2   = sort_level(tc->ensure_type(A).first);
-        expr eqrec = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, rhs, motive, minor, lhs, major});
-        if (has_dep_elim) {
+        name eq_rec_name;
+        if (!has_dep_elim && use_dep_elim)
+            eq_rec_name = get_eq_drec_name();
+        else
+            eq_rec_name = get_eq_rec_name();
+        expr eqrec = mk_app({mk_constant(eq_rec_name, {l1, l2}), A, rhs, motive, minor, lhs, major});
+        if (use_dep_elim) {
             try {
                 check_term(env, g.abstract(eqrec));
             } catch (kernel_exception & ex) {
diff --git a/tests/lean/run/dep_subst.lean b/tests/lean/run/dep_subst.lean
new file mode 100644
index 0000000000..3e14134e5e
--- /dev/null
+++ b/tests/lean/run/dep_subst.lean
@@ -0,0 +1,28 @@
+import data.finset
+open subtype setoid finset set
+
+inductive finite_set [class] {T : Type} (xs : set T) :=
+| mk : ∀ (fxs : finset T), to_set fxs = xs → finite_set xs
+
+definition card {T : Type} (xs : set T) [fn : finite_set xs] : nat :=
+begin
+  induction fn,
+  exact finset.card fxs
+end
+
+example {T : Type} (xs : set T) [fn₁ fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
+begin
+  induction fn₁ with fxs₁ h₁,
+  induction fn₂ with fxs₂ h₂,
+  subst xs,
+  apply sorry
+end
+
+example {T : Type} (xs : set T) [fn₁ fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
+begin
+  induction fn₁ with fxs₁ h₁,
+  induction fn₂ with fxs₂ h₂,
+  subst xs,
+  let aux := to_set.inj h₂,
+  subst aux
+end