diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp
index 6ab003836..86f4c9ffa 100644
--- a/src/library/blast/forward/pattern.cpp
+++ b/src/library/blast/forward/pattern.cpp
@@ -40,7 +40,7 @@ patterns used by heuristic instantiation.
      a_i is NOT trackable.
      Reason: we can infer a_i from a_j using type inference.
 
-  b) a_i is a proposition -> a_i is NOT trackable.
+  b) a_i is a non dependent proposition -> a_i is NOT trackable.
      Reason: we can leave a_i as hypothesis whenever we instantiate H.
 
   c) a_i is instance implicit -> a_i is NOT trackable.
@@ -214,9 +214,10 @@ expr extract_trackable(tmp_type_context & ctx, expr const & type,
         bool is_inst_implicit = binding_info(it).is_inst_implicit();
         inst_implicit_flags.push_back(is_inst_implicit);
         bool is_prop          = ctx.is_prop(binding_domain(it));
+        bool dep              = !closed(binding_body(it));
         if (!is_inst_implicit) {
             unsigned midx = to_meta_idx(new_mvar);
-            if (is_prop)
+            if (is_prop && !dep)
                 residue.insert(midx);
             else
                 trackable.insert(midx);
diff --git a/tests/lean/run/blast_flat.lean b/tests/lean/run/blast_flat.lean
new file mode 100644
index 000000000..c16b6eea2
--- /dev/null
+++ b/tests/lean/run/blast_flat.lean
@@ -0,0 +1,21 @@
+open nat subtype
+
+definition f (x : nat) (y : {n : nat | n > x}) : nat :=
+x + elt_of y
+
+definition f_flat (x : nat) (y : nat) (H : y > x) : nat :=
+f x (tag y H)
+
+lemma f_flat_simp [forward] (x : nat) (y : nat) (H : y > x) : f x (tag y H) = f_flat x y H :=
+rfl
+
+set_option trace.simplifier true
+set_option trace.blast true
+set_option blast.strategy "ematch"
+
+example (a b c d : nat) (Ha : c > a) (Hb : d > b) : a = b → c = d → f a (tag c Ha) = f b (tag d Hb) :=
+by blast
+
+example (h : nat → nat) (a b c d : nat) (Ha : h c > h a) (Hb : h d > h b)
+        : h a = h b → c = d → f (h a) (tag (h c) Ha) = f (h b) (tag (h d) Hb) :=
+by blast