diff --git a/tests/lean/run/blast_cc4.lean b/tests/lean/run/blast_cc4.lean
new file mode 100644
index 0000000000..b4bf66ed0c
--- /dev/null
+++ b/tests/lean/run/blast_cc4.lean
@@ -0,0 +1,11 @@
+open nat
+set_option blast.subst false
+
+definition tst
+        (a₁ a₂ b₁ b₂ c d : nat) :
+        a₁ = c → a₂ = c →
+        b₁ = d → d  = b₂ →
+        a₁ + b₁ + a₁ = a₂ + b₂ + c :=
+by blast
+
+print tst