1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/Case1.v b/test-suite/success/Case1.v
new file mode 100644
index 00000000..2d5a5134
--- /dev/null
+++ b/test-suite/success/Case1.v
@@ -0,0 +1,15 @@
+(* Testing eta-expansion of elimination predicate *)
+
+Section NATIND2.
+Variable P : nat -> Type.
+Variable H0 : (P O).
+Variable H1 : (P (S O)).
+Variable H2 : (n:nat)(P n)->(P (S (S n))).
+Fixpoint nat_ind2 [n:nat] : (P n) :=
+         <P>Cases n of  
+                        O     => H0
+                  | (S O)     => H1
+                  | (S (S n)) => (H2 n (nat_ind2 n))
+        end.
+End NATIND2.
+