1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v
new file mode 100644
index 00000000..6e2aea48
--- /dev/null
+++ b/test-suite/success/Case7.v
@@ -0,0 +1,16 @@
+Inductive List [A:Set] :Set := 
+ Nil:(List A) | Cons:A->(List A)->(List A).
+
+Inductive Empty [A:Set] : (List A)-> Prop := 
+  intro_Empty: (Empty A (Nil A)).
+
+Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)).
+
+
+Type
+[A:Set] 
+[l:(List A)]
+  <[l:(List A)](Empty A l) \/ ~(Empty A l)>Cases l of 
+        Nil  =>  (or_introl ? ~(Empty A (Nil A)) (intro_Empty A))
+   |  ((Cons a y) as b) =>  (or_intror (Empty A b) ? (inv_Empty A a y))
+  end.