From d736376a6f30a487ca64768551d04b776fd0debe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Jan 2016 16:50:03 -0800
Subject: [PATCH] test(tests/lean/run/blast_cc_heq8): new congruence closure
 procedure can also handle subtypes without using a flattening preprocessing
 step

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

diff --git a/tests/lean/run/blast_cc_heq8.lean b/tests/lean/run/blast_cc_heq8.lean
new file mode 100644
index 0000000000..a90ad66722
--- /dev/null
+++ b/tests/lean/run/blast_cc_heq8.lean
@@ -0,0 +1,10 @@
+open nat subtype
+
+definition f (x : nat) (y : {n : nat | n > x}) : nat :=
+x + elt_of y
+
+set_option blast.subst false
+
+example (h : nat → nat) (a b c d : nat) (Ha : h c > h a) (Hb : h d > h b)
+        : h a = h b → c = d → f (h a) (tag (h c) Ha) = f (h b) (tag (h d) Hb) :=
+by inst_simp