diff --git a/tests/lean/run/blast_ematch9.lean b/tests/lean/run/blast_ematch9.lean
new file mode 100644
index 000000000..450e2671b
--- /dev/null
+++ b/tests/lean/run/blast_ematch9.lean
@@ -0,0 +1,8 @@
+constant P : nat → Prop
+definition h [reducible] (n : nat) := n
+definition foo [forward] : ∀ x, P (h x) := sorry
+
+set_option blast.ematch true
+
+example (n : nat) : P (h n) :=
+by blast