From 2627eade8b171d1e6316d0ce0ad0a680b8a10b2b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Nov 2015 13:53:36 -0800
Subject: [PATCH] test(tests/lean/run/blast_cc3): add test for
 congruence_closure with dependent types

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

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