diff --git a/tests/lean/run/blast_simp4.lean b/tests/lean/run/blast_simp4.lean
new file mode 100644
index 0000000000..0b5d5e89c1
--- /dev/null
+++ b/tests/lean/run/blast_simp4.lean
@@ -0,0 +1,15 @@
+import data.nat
+open nat
+
+constant f : nat → nat
+definition g (a : nat) := a
+
+
+example (a b : nat) : a + 0 = 0 + g b → f (f b) = f (f a) :=
+suppose a + 0 = 0 + g b,
+assert a = b, by unfold g at *; simp,
+by simp
+
+attribute g [reducible]
+example (a b : nat) : a + 0 = 0 + g b → f (f b) = f (f a) :=
+by simp