From eb3d73873ad84d84e20cce1717ef8eeb134b5c5b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Nov 2015 14:01:15 -0800
Subject: [PATCH] test(tests/lean/run/blast_cc4): congruence_closure and type
 classes

---
 tests/lean/run/blast_cc4.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 tests/lean/run/blast_cc4.lean

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