diff --git a/tests/lean/run/blast_cc3.lean b/tests/lean/run/blast_cc3.lean
new file mode 100644
index 000000000..74e081e74
--- /dev/null
+++ b/tests/lean/run/blast_cc3.lean
@@ -0,0 +1,15 @@
+open nat
+set_option blast.subst false
+constant f (a b : nat) : a > b → nat
+constant g : nat → nat
+
+definition tst
+        (a₁ a₂ b₁ b₂ c d : nat)
+        (H₁ : a₁ > b₁)
+        (H₂ : a₂ > b₂) :
+        a₁ = c → a₂ = c →
+        b₁ = d → d  = b₂ →
+        g (g (f a₁ b₁ H₁)) = g (g (f a₂ b₂ H₂)) :=
+by blast
+
+print tst