Comportements peut-être souhaités mais en tout cas non officiellement pris en compte

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1995 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 2118 insertions, 0 deletions

diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v
new file mode 100644
index 000000000..e80e95bfa
--- /dev/null
+++ b/test-suite/ideal-features/Apply.v
@@ -0,0 +1,26 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* This needs unification on type *)
+
+Goal (n,m:nat)(eq nat (S m) (S n)).
+Intros.
+Apply f_equal.
+
+(* f_equal : (A,B:Set; f:(A->B); x,y:A)x=y->(f x)=(f y) *)
+(* and A cannot be deduced from the goal but only from the type of f, x or y *)
+
+
+(* This needs step by step unfolding *)
+
+Fixpoint T [n:nat] : Prop := Cases n of O => True | (S p) => n=n->(T p) end.
+Require Arith.
+
+Goal (T (3))->(T (1)).
+Intro H.
+Apply H.
diff --git a/test-suite/ideal-features/Case3.v b/test-suite/ideal-features/Case3.v
new file mode 100644
index 000000000..e9dba1e3f
--- /dev/null
+++ b/test-suite/ideal-features/Case3.v
@@ -0,0 +1,28 @@
+Inductive Le : nat->nat->Set :=
+  LeO: (n:nat)(Le O n) 
+| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)).
+
+Parameter iguales : (n,m:nat)(h:(Le n m))Prop .
+
+Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of 
+                         (LeO O) => True
+                       | (LeS (S x) (S y) H) => (iguales (S x) (S y) H)
+                       | _ => False end.
+
+
+Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of 
+                         (LeO O) => True
+                       | (LeS (S x) O H) => (iguales (S x) O H)
+                       | _ => False end.
+
+Parameter discr_l : (n:nat) ~((S n)=O).
+
+Type 
+[n:nat] 
+  <[n:nat]n=O\/~n=O>Cases n of 
+      O     => (or_introl ? ~O=O (refl_equal ? O))      
+   |  (S O) => (or_intror (S O)=O ? (discr_l O))
+   |  (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x)))
+ 
+  end.
+
diff --git a/test-suite/ideal-features/Case4.v b/test-suite/ideal-features/Case4.v
new file mode 100644
index 000000000..d8f14a4e1
--- /dev/null
+++ b/test-suite/ideal-features/Case4.v
@@ -0,0 +1,39 @@
+Inductive listn : nat-> Set := 
+  niln : (listn O) 
+| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+
+Inductive empty : (n:nat)(listn n)-> Prop := 
+  intro_empty: (empty O niln).
+
+Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
+
+Type 
+[n:nat] [l:(listn n)]
+  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
+        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
+   |  ((consn n O y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n O y))
+   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
+
+  end.
+
+
+Type 
+[n:nat] [l:(listn n)]
+  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
+        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
+   |  (consn n O y)  =>  (or_intror (empty (S n) (consn n O y)) ? 
+                                              (inv_empty n O y))
+   |  (consn n a y) =>  (or_intror (empty (S n) (consn n a y)) ? 
+                                          (inv_empty n a y))
+
+  end.
+
+Type 
+[n:nat] [l:(listn n)]
+  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
+        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
+   |  ((consn O a y) as b) =>  (or_intror (empty (S O) b) ? (inv_empty O a y))
+   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
+
+  end.
+
diff --git a/test-suite/ideal-features/Case5.v b/test-suite/ideal-features/Case5.v
new file mode 100644
index 000000000..d703286f9
--- /dev/null
+++ b/test-suite/ideal-features/Case5.v
@@ -0,0 +1,15 @@
+
+Reset ff.
+Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m).
+Parameter discr_r : (n:nat) ~(O=(S n)).
+Parameter discr_l : (n:nat) ~((S n)=O).
+
+
+Type 
+[n:nat] 
+  <[n:nat]n=O\/~n=O>Cases n of 
+      O     => (or_introl ? ~O=O (refl_equal ? O))      
+   |  (S O) => (or_intror (S O)=O ? (discr_l O))
+   |  (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x)))
+ 
+  end.
diff --git a/test-suite/ideal-features/Case8.v b/test-suite/ideal-features/Case8.v
new file mode 100644
index 000000000..73b55028d
--- /dev/null
+++ b/test-suite/ideal-features/Case8.v
@@ -0,0 +1,40 @@
+Inductive listn : nat-> Set := 
+  niln : (listn O) 
+| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+
+Inductive empty : (n:nat)(listn n)-> Prop := 
+  intro_empty: (empty O niln).
+
+Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
+
+Type 
+[n:nat] [l:(listn n)]
+  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
+        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
+   |  ((consn n O y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n O y))
+   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
+
+  end.
+
+
+Type 
+[n:nat] [l:(listn n)]
+  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
+        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
+   |  (consn n O y)  =>  (or_intror (empty (S n) (consn n O y)) ? 
+                                              (inv_empty n O y))
+   |  (consn n a y) =>  (or_intror (empty (S n) (consn n a y)) ? 
+                                          (inv_empty n a y))
+
+  end.
+
+
+
+Type 
+[n:nat] [l:(listn n)]
+  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
+        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
+   |  ((consn O a y) as b) =>  (or_intror (empty (S O) b) ? (inv_empty O a y))
+   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
+
+  end.
diff --git a/test-suite/ideal-features/Cases.v b/test-suite/ideal-features/Cases.v
new file mode 100644
index 000000000..313f8f74a
--- /dev/null
+++ b/test-suite/ideal-features/Cases.v
@@ -0,0 +1,1596 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(****************************************************************************)
+(* Pattern-matching when non inductive terms occur                          *)
+
+(* Dependent form of annotation *)
+Type <[n:nat]nat>Cases O eq of O x => O | (S x) y => x end.
+Type <[_,_:nat]nat>Cases O eq O of O x y => O | (S x) y z => x end.
+
+(* Non dependent form of annotation *)
+Type <nat>Cases O eq of O x => O | (S x) y => x end.
+
+(****************************************************************************)
+(* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v   *)
+
+Inductive IFExpr : Set := 
+          Var  : nat -> IFExpr
+        | Tr   : IFExpr
+        | Fa   : IFExpr
+        | IfE   : IFExpr -> IFExpr -> IFExpr -> IFExpr.
+
+Inductive List [A:Set] :Set := 
+ Nil:(List A) | Cons:A->(List A)->(List A).
+
+Inductive listn : nat-> Set := 
+  niln : (listn O) 
+| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+
+Inductive Listn [A:Set] : nat-> Set := 
+  Niln : (Listn A O) 
+| Consn : (n:nat)nat->(Listn A n) -> (Listn A (S n)).
+
+Inductive Le : nat->nat->Set :=
+  LeO: (n:nat)(Le O n) 
+| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)).
+
+Inductive LE [n:nat] : nat->Set := 
+    LE_n : (LE n n) | LE_S : (m:nat)(LE n m)->(LE n (S m)).
+
+Require Bool.
+
+
+
+Inductive PropForm : Set := 
+          Fvar : nat -> PropForm
+        | Or   : PropForm -> PropForm -> PropForm .
+
+Section testIFExpr.
+Definition  Assign:= nat->bool.
+Parameter Prop_sem : Assign -> PropForm -> bool.
+
+Type [A:Assign][F:PropForm] 
+    <bool>Cases F of
+           (Fvar n)   => (A n)
+         | (Or F G)   => (orb (Prop_sem A F) (Prop_sem A G))
+    end.
+
+Type [A:Assign][H:PropForm] 
+    <bool>Cases H of
+           (Fvar n)   => (A n)
+         | (Or F G)   => (orb (Prop_sem A F) (Prop_sem A G))
+    end.
+End testIFExpr.
+
+
+
+Type [x:nat]<nat>Cases x of O => O | x => x end.
+
+Section testlist.
+Parameter A:Set.
+Inductive list : Set := nil : list | cons : A->list->list.
+Parameter inf: A->A->Prop.
+
+
+Definition list_Lowert2 :=
+   [a:A][l:list](<Prop>Cases l of nil => True 
+                               | (cons b l) =>(inf a b) end).
+
+Definition titi :=
+   [a:A][l:list](<list>Cases l of nil => l
+                               | (cons b l) => l end).
+Reset list.
+End testlist.
+
+
+(* To test translation *)
+(* ------------------- *)
+
+
+Type  <nat>Cases O of O => O | _ => O end.
+
+Type <nat>Cases O of
+               (O as b) => b 
+             | (S O)  => O
+             | (S (S x)) => x end.
+
+Type Cases O of
+               (O as b) => b 
+             | (S O)  => O
+             | (S (S x)) => x end.
+
+
+Type [x:nat]<nat>Cases x of
+                          (O as b) => b 
+                        | (S x)  => x end.
+
+Type              [x:nat]Cases x of
+                          (O as b) => b 
+                        | (S x)  => x end.
+
+Type <nat>Cases O of 
+                          (O as b) => b 
+                        | (S x)  => x end.
+
+Type <nat>Cases O of 
+                          x  => x 
+                       end.
+
+Type  Cases O of 
+                          x  => x 
+                       end.
+
+Type <nat>Cases O of
+                              O => O
+                         | ((S x) as b) => b
+                        end.
+
+Type [x:nat]<nat>Cases x of
+                              O => O
+                         | ((S x) as b) => b
+                        end.
+
+Type [x:nat] Cases x of
+                              O => O
+                         | ((S x) as b) => b
+                        end.
+
+
+Type <nat>Cases O of
+         O => O
+    | (S x) => O
+      end.
+
+
+Type <nat*nat>Cases O of
+                              O => (O,O)
+                         | (S x) =>  (x,O)
+                        end.
+
+Type                    Cases O of
+                              O => (O,O)
+                         | (S x) =>  (x,O)
+                        end.
+
+Type <nat->nat>Cases O of
+                              O => [n:nat]O
+                         | (S x) =>  [n:nat]O
+                        end.
+
+Type                   Cases O of
+                              O => [n:nat]O
+                         | (S x) =>  [n:nat]O
+                        end.
+
+
+Type <nat->nat>Cases O of
+                              O => [n:nat]O
+                         | (S x) =>  [n:nat](plus x n)
+                        end.
+
+Type                    Cases O of
+                              O => [n:nat]O
+                         | (S x) =>  [n:nat](plus x n)
+                        end.
+
+
+Type <nat>Cases O of
+                              O => O
+                         | ((S x) as b) => (plus b x)
+                         end.
+
+Type <nat>Cases O of
+              O => O
+          | ((S (x as a)) as b) => (plus b a)
+                         end.
+Type  Cases O of
+              O => O
+          | ((S (x as a)) as b) => (plus b a)
+                         end.
+
+
+Type  Cases O of
+                              O => O
+                         |  _  => O
+                        end.
+
+Type <nat>Cases O of
+                  O => O
+               |  x => x
+                 end.
+
+Type <nat>Cases O (S O) of
+                             x  y => (plus x y)
+                        end.
+
+Type      Cases O (S O) of
+                             x  y => (plus x y)
+                        end.
+ 
+Type <nat>Cases O (S O) of
+                             O  y => y
+                          | (S x) y => (plus x y) 
+                        end.
+
+Type              Cases O (S O) of
+                             O  y => y
+                          | (S x) y => (plus x y) 
+                        end.
+
+
+Type    <nat>Cases O (S O) of
+                      O  x =>  x
+             |      (S y) O =>  y
+             |        x y  => (plus x y)
+           end.
+
+
+
+
+Type        Cases O (S O) of
+                      O  x => (plus x O)
+             |      (S y) O =>  (plus y O)
+             |        x y  => (plus x y)
+           end.
+
+Type 
+          <nat>Cases O (S O) of
+                      O  x => (plus x O)
+             |      (S y) O =>  (plus y O)
+             |        x y  => (plus x y)
+           end.
+
+
+Type 
+          <nat>Cases O (S O) of
+                      O  x =>  x 
+             | ((S x) as b) (S y) => (plus (plus b x) y)
+             |    x y  => (plus x y)
+           end.
+
+
+Type         Cases O (S O) of
+                    O  x =>  x 
+             | ((S x) as b) (S y) => (plus (plus b x) y)
+             |    x y  => (plus x y)
+           end.
+
+
+Type [l:(List nat)]<(List nat)>Cases l of 
+                         Nil => (Nil nat)
+                      | (Cons  a l) => l
+                      end.
+
+Type [l:(List nat)]  Cases l of 
+                         Nil => (Nil nat)
+                      | (Cons  a l) => l
+                      end.
+
+Type <nat>Cases (Nil nat) of 
+                         Nil =>O
+                      | (Cons  a l) => (S a)
+                      end.
+Type Cases (Nil nat) of 
+                         Nil =>O
+                      | (Cons  a l) => (S a)
+                      end.
+
+Type <(List nat)>Cases (Nil nat) of 
+                        (Cons  a l) => l
+                       | x => x
+                      end.
+
+Type              Cases (Nil nat) of 
+                        (Cons  a l) => l
+                       | x => x
+                      end.
+
+Type <(List nat)>Cases (Nil nat) of 
+                         Nil => (Nil nat)
+                      | (Cons  a l) => l
+                      end.
+
+Type             Cases (Nil nat) of 
+                         Nil => (Nil nat)
+                      | (Cons  a l) => l
+                      end.
+
+
+Type 
+   <nat>Cases O of 
+      O => O
+    | (S x) => <nat>Cases (Nil nat) of 
+                         Nil => x
+                      | (Cons  a l) => (plus x a)
+                      end
+     end.
+
+Type 
+   Cases O of 
+      O => O
+    | (S x) => Cases (Nil nat) of 
+                         Nil => x
+                      | (Cons  a l) => (plus x a)
+                      end
+     end.
+
+Type 
+ [y:nat]Cases y of 
+      O => O
+    | (S x) => Cases (Nil nat) of 
+                         Nil => x
+                      | (Cons  a l) => (plus x a)
+                      end
+     end.
+
+
+Type 
+   <nat>Cases O (Nil nat) of 
+      O       x => O
+    | (S x)  Nil => x
+    | (S x) (Cons  a l) => (plus x a)      
+     end.
+
+
+
+Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of 
+                         niln => O
+                      |    x  => O
+                      end.
+
+Type [n:nat][l:(listn n)]
+                     Cases l of 
+                         niln => O
+                      |    x  => O
+                      end.
+
+
+Type <[_:nat]nat>Cases niln of 
+                         niln => O
+                      |    x  => O
+                      end.
+
+Type               Cases niln of 
+                         niln => O
+                      |    x  => O
+                      end.
+
+
+Type <[_:nat]nat>Cases niln of 
+                         niln => O
+                      |  (consn n a l)  => a
+                      end.
+Type Cases niln of niln => O
+               |  (consn n a l)  => a
+     end.
+
+
+Type  <[n:nat][_:(listn n)]nat>Cases niln of 
+                         (consn m _ niln) => m
+                       | _ => (S O) end.
+
+
+
+Type [n:nat][x:nat][l:(listn n)]<[_:nat]nat>Cases x l of 
+                         O niln => O
+                      |  y  x  => O
+                      end.
+
+Type <[_:nat]nat>Cases O niln of 
+                         O niln => O
+                      |  y  x  => O
+                      end.
+
+
+Type <[_:nat]nat>Cases niln O of 
+                         niln O => O
+                      |  y  x  => O
+                      end.
+
+Type               Cases niln O of 
+                         niln O => O
+                      |  y  x  => O
+                      end.
+
+Type <[_:nat][_:nat]nat>Cases niln niln of 
+                         niln niln => O
+                      |    x  y  => O
+                      end.
+
+Type               Cases niln niln of 
+                         niln niln => O
+                      |    x  y  => O
+                      end.
+
+Type <[_,_,_:nat]nat>Cases niln niln niln of 
+                         niln niln niln => O
+                      |    x  y z  => O
+                      end.
+
+
+Type                 Cases niln niln niln of 
+                         niln niln niln => O
+                      |    x  y z  => O
+                      end.
+
+
+
+Type <[_:nat]nat>Cases (niln) of 
+                         niln  => O
+                      | (consn n a l) => O
+                      end.
+
+Type         Cases (niln) of 
+                         niln  => O
+                      | (consn n a l) => O
+                      end.
+
+
+Type <[_:nat][_:nat]nat>Cases niln niln of 
+                         niln niln => O
+                      |  niln (consn n a l) => n
+                      |  (consn n a l)  x  => a
+                      end.
+
+
+Type                Cases niln niln of 
+                         niln niln => O
+                      |  niln (consn n a l) => n
+                      |  (consn n a l)  x  => a
+                      end.
+
+
+Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of 
+                         niln => O
+                      |    x  => O
+                      end.
+
+Type [c:nat;s:bool]
+  <[_:nat;_:bool]nat>Cases c s of
+        | O _ => O
+        | _ _ => c
+        end.
+
+Type [c:nat;s:bool]
+  <[_:nat;_:bool]nat>Cases c s of
+        | O _ => O
+        | (S _) _ => c
+        end.
+         
+
+(* Rows of pattern variables: some tricky cases *)
+Axiom P:nat->Prop; f:(n:nat)(P n).
+
+Type [i:nat]
+  <[_:bool;n:nat](P n)>Cases true i of
+        | true k => (f k)
+        | _    k => (f k)
+        end.
+
+Type [i:nat]
+  <[n:nat;_:bool](P n)>Cases i true of
+        | k true => (f k)
+        | k _ => (f k)
+        end.
+
+(* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe
+ * it has to synthtize the predicate on O (which he can't)
+ *)
+Type <[n]Cases n of O => bool | (S _) => nat end>Cases O of
+    O => true
+  | (S _) => O
+  end.
+
+Type [n:nat][l:(listn n)]Cases l of 
+                         niln => O
+                      |    x  => O
+                      end.
+
+Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of 
+                         niln  => O
+                      | (consn n a niln) => O
+                      | (consn n a (consn m b l)) => (plus n m)
+                      end.
+
+
+Type [n:nat][l:(listn n)]Cases l of 
+                         niln  => O
+                      | (consn n a niln) => O
+                      | (consn n a (consn m b l)) => (plus n m)
+                      end.
+
+
+
+Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of 
+                         niln  => O
+                      | (consn n a niln) => O
+                      | (consn n a (consn m b l)) => (plus n m)
+                      end.
+
+Type [n:nat][l:(listn n)]Cases l of 
+                         niln  => O
+                      | (consn n a niln) => O
+                      | (consn n a (consn m b l)) => (plus n m)
+                      end.
+
+
+Type [A:Set][n:nat][l:(Listn A n)]<[_:nat]nat>Cases l of 
+                         Niln   => O
+                      | (Consn n a Niln) => O
+                      | (Consn n a (Consn m b l)) => (plus n m)
+                      end.
+
+Type [A:Set][n:nat][l:(Listn A n)]Cases l of 
+                         Niln   => O
+                      | (Consn n a Niln) => O
+                      | (Consn n a (Consn m b l)) => (plus n m)
+                      end.
+
+(*
+Type [A:Set][n:nat][l:(Listn A n)]
+                   <[_:nat](Listn A O)>Cases l of 
+                         (Niln  as b) => b
+                      | (Consn  n a (Niln  as b))=> (Niln A)
+                      | (Consn  n a (Consn m b l)) => (Niln A)
+                      end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+                    Cases l of 
+                         (Niln  as b) => b
+                      | (Consn  n a (Niln  as b))=> (Niln A)
+                      | (Consn  n a (Consn m b l)) => (Niln A)
+                      end.
+*)
+(******** This example rises an error unconstrained_variables!
+Type [A:Set][n:nat][l:(Listn A n)]
+                    Cases l of 
+                         (Niln  as b) => (Consn A O O b)
+                      | ((Consn  n a Niln) as L) =>  L 
+                      | (Consn  n a _)  =>  (Consn A O O (Niln A))
+                      end.
+**********)
+
+(* To test tratement of as-patterns in depth *)
+Type [A:Set] [l:(List A)]
+                    Cases l of 
+                         (Nil  as b) => (Nil A)
+                      | ((Cons a Nil)  as L) => L
+                      | ((Cons a (Cons b m)) as L) => L
+                      end.
+
+
+Type [n:nat][l:(listn n)]
+             <[_:nat](listn n)>Cases l of 
+                         niln  => l 
+                      | (consn n a c) => l
+                      end.
+Type [n:nat][l:(listn n)]
+                      Cases l of 
+                         niln  => l 
+                      | (consn n a c) => l
+                      end.
+
+
+Type [n:nat][l:(listn n)]
+             <[_:nat](listn n)>Cases l of 
+                         (niln as b) => l 
+                      |  _  => l
+                      end.
+
+
+Type [n:nat][l:(listn n)]
+                     Cases l of 
+                         (niln as b) => l 
+                      |  _  => l
+                      end.
+
+Type [n:nat][l:(listn n)]
+             <[_:nat](listn n)>Cases l of 
+                         (niln as b) => l
+                      |  x  => l
+                      end.
+
+
+Type [A:Set][n:nat][l:(Listn A n)]
+                       Cases l of 
+                         (Niln  as b) => l 
+                      |   _ => l
+                      end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+             <[_:nat](Listn A n)>Cases l of 
+                         Niln  => l 
+                      | (Consn  n a Niln) => l
+                      | (Consn  n a (Consn  m b c)) => l 
+                      end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+                      Cases l of 
+                         Niln  => l 
+                      | (Consn  n a Niln) => l
+                      | (Consn  n a (Consn  m b c)) => l 
+                      end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+             <[_:nat](Listn A n)>Cases l of 
+                         (Niln as b) => l 
+                      | (Consn  n a (Niln as b)) => l
+                      | (Consn  n a (Consn  m b _)) => l 
+                      end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+                     Cases l of 
+                         (Niln as b) => l 
+                      | (Consn  n a (Niln as b)) => l
+                      | (Consn  n a (Consn  m b _)) => l 
+                      end.
+
+
+Type <[_:nat]nat>Cases (niln) of 
+                         niln  => O
+                      | (consn n a niln) => O
+                      | (consn n a (consn m b l)) => (plus n m)
+                      end.
+
+
+Type               Cases (niln) of 
+                         niln  => O
+                      | (consn n a niln) => O
+                      | (consn n a (consn m b l)) => (plus n m)
+                      end.
+
+Type <[_,_:nat]nat>Cases (LeO O) of 
+                         (LeO x)  => x
+                      | (LeS n m h) => (plus n m) 
+                      end.
+
+
+Type               Cases (LeO O) of 
+                         (LeO x)  => x
+                      | (LeS n m h) => (plus n m) 
+                      end.
+
+Type [n:nat][l:(Listn nat n)]
+                     <[_:nat]nat>Cases l of 
+                         Niln  => O
+                      | (Consn n a l) => O
+                      end.
+
+
+Type [n:nat][l:(Listn nat n)]
+                      Cases l of 
+                         Niln  => O
+                      | (Consn n a l) => O
+                      end.
+
+
+Type                Cases (Niln nat) of 
+                         Niln  => O
+                      | (Consn n a l) => O
+                      end.
+
+Type <[_:nat]nat>Cases (LE_n O) of 
+                         LE_n   => O 
+                      | (LE_S m h) => O
+                      end.
+
+
+Type               Cases (LE_n O) of 
+                         LE_n   => O 
+                      | (LE_S m h) => O
+                      end.
+
+
+
+Type               Cases (LE_n O) of 
+                         LE_n   => O 
+                      | (LE_S m h) => O
+                      end.
+
+
+
+Type <[_:nat]nat>Cases (niln ) of 
+                         niln   => O
+                      | (consn  n a niln) => n
+                      | (consn  n a (consn  m b l)) => (plus n m)
+                      end.
+
+Type               Cases (niln ) of 
+                         niln   => O
+                      | (consn  n a niln) => n
+                      | (consn  n a (consn  m b l)) => (plus n m)
+                      end.
+
+
+Type <[_:nat]nat>Cases (Niln nat) of 
+                         Niln  => O
+                      | (Consn  n a Niln) => n
+                      | (Consn   n a (Consn  m b l)) => (plus n m)
+                      end.
+
+Type                Cases (Niln nat) of 
+                         Niln  => O
+                      | (Consn  n a Niln) => n
+                      | (Consn   n a (Consn  m b l)) => (plus n m)
+                      end.
+
+
+Type <[_,_:nat]nat>Cases (LeO O) of 
+                         (LeO x)  => x
+                      | (LeS n m (LeO x)) => (plus x m)
+                      | (LeS n m (LeS x y h)) => (plus n x)
+                      end.
+
+
+Type                 Cases (LeO O) of 
+                         (LeO x)  => x
+                      | (LeS n m (LeO x)) => (plus x m)
+                      | (LeS n m (LeS x y h)) => (plus n x)
+                      end.
+
+
+Type <[_,_:nat]nat>Cases (LeO O) of 
+                         (LeO x)  => x
+                      | (LeS n m (LeO x)) => (plus x m)
+                      | (LeS n m (LeS x y h)) => m
+                      end.
+
+Type                Cases (LeO O) of 
+                         (LeO x)  => x
+                      | (LeS n m (LeO x)) => (plus x m)
+                      | (LeS n m (LeS x y h)) => m
+                      end.
+
+
+Type [n,m:nat][h:(Le n m)]
+                    <[_,_:nat]nat>Cases h of 
+                         (LeO x)  => x
+                      | x => O
+                      end.
+
+Type [n,m:nat][h:(Le n m)]
+                     Cases h of 
+                         (LeO x)  => x
+                      | x => O
+                      end.
+
+
+Type [n,m:nat][h:(Le n m)]
+                    <[_,_:nat]nat>Cases h of 
+                        (LeS n m h)  => n
+                      | x => O
+                      end.
+
+
+Type [n,m:nat][h:(Le n m)]
+                      Cases h of 
+                        (LeS n m h)  => n
+                      | x => O
+                      end.
+
+
+Type    [n,m:nat][h:(Le n m)]
+  <[_,_:nat]nat*nat>Cases h of
+                    (LeO n) => (O,n)
+                   |(LeS n m _) => ((S n),(S m))
+                   end.
+
+
+Type    [n,m:nat][h:(Le n m)]
+                  Cases h of
+                    (LeO n) => (O,n)
+                   |(LeS n m _) => ((S n),(S m))
+                   end.
+
+
+Fixpoint F [n,m:nat; h:(Le n m)] : (Le n (S m)) :=
+ <[n,m:nat](Le n (S m))>Cases h  of 
+                (LeO m') => (LeO (S m'))
+              | (LeS n' m' h') => (LeS n' (S m') (F n' m' h'))
+        end.
+
+Reset F.
+
+Fixpoint F [n,m:nat; h:(Le n m)] :(Le n (S m)) :=
+  <[n,m:nat](Le n (S m))>Cases h of
+                           (LeS n m h) => (LeS n (S m) (F n m h))
+                         | (LeO m) => (LeO (S m)) 
+                        end.
+
+(* Rend la longueur de la liste *)
+Definition length1:= [n:nat] [l:(listn n)]
+        <[_:nat]nat>Cases l of 
+                     (consn n _ (consn m _ _)) => (S (S m))
+                    |(consn n _ _) => (S O)
+                    | _ => O
+             end.
+
+Reset length1.
+Definition length1:= [n:nat] [l:(listn n)]
+                    Cases l of 
+                     (consn n _ (consn m _ _)) => (S (S m))
+                    |(consn n _ _) => (S O)
+                    | _ => O
+                    end.
+
+
+Definition length2:= [n:nat] [l:(listn n)]
+        <[_:nat]nat>Cases l of 
+                     (consn n _ (consn m _ _)) => (S (S m))
+                    |(consn n _ _) => (S n)
+                    | _ => O
+             end.
+
+Reset length2.
+
+Definition length2:= [n:nat] [l:(listn n)]
+                   Cases l of 
+                     (consn n _ (consn m _ _)) => (S (S m))
+                    |(consn n _ _) => (S n)
+                    | _ => O
+                   end.
+
+Definition length3 :=
+[n:nat][l:(listn n)]
+        <[_:nat]nat>Cases l of 
+                     (consn n _ (consn m _ l)) => (S n)
+                    |(consn n _ _) => (S O)
+                    | _  => O
+                   end.
+
+
+Reset length3.
+
+Definition length3 :=
+[n:nat][l:(listn n)]
+                   Cases l of 
+                     (consn n _ (consn m _ l)) => (S n)
+                    |(consn n _ _) => (S O)
+                    | _  => O
+                   end.
+
+ 
+Type <[_,_:nat]nat>Cases (LeO O) of 
+                        (LeS n m h)  =>(plus n m)
+                      | x => O
+                      end.
+Type              Cases (LeO O) of 
+                        (LeS n m h)  =>(plus n m)
+                      | x => O
+                      end.
+
+Type [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of 
+                         (LeO x)  => x
+                      | (LeS n m (LeO x)) => (plus x m)
+                      | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y)))
+                      end.
+
+
+Type [n,m:nat][h:(Le n m)]Cases h of 
+                         (LeO x)  => x
+                      | (LeS n m (LeO x)) => (plus x m)
+                      | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y)))
+                      end.
+
+Type <[_,_:nat]nat>Cases (LeO O) of 
+                         (LeO x)  => x
+                      | (LeS n m (LeO x)) => (plus x m)
+                      | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y)))
+                      end.
+
+Type                 Cases (LeO O) of 
+                         (LeO x)  => x
+                      | (LeS n m (LeO x)) => (plus x m)
+                      | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y)))
+                      end.
+
+
+Type <[_:nat]nat>Cases (LE_n O) of 
+                         LE_n   => O
+                      | (LE_S m LE_n) => (plus O m)
+                      | (LE_S m (LE_S y h)) => (plus O m)
+                      end.
+
+
+Type                Cases (LE_n O) of 
+                         LE_n   => O
+                      | (LE_S m LE_n) => (plus O m)
+                      | (LE_S m (LE_S y h)) => (plus O m)
+                      end.
+
+
+Type [n,m:nat][h:(Le n m)]              Cases h of 
+                                                x => x 
+                                          end.
+
+Type [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of 
+                                               (LeO n) => n
+                                              |   x => O
+                                          end.
+Type [n,m:nat][h:(Le n m)] Cases h of 
+                               (LeO n) => n
+                             |   x => O
+                            end.
+
+
+Type [n:nat]<[_:nat]nat->nat>Cases niln of 
+                         niln  => [_:nat]O
+                      | (consn n a niln) => [_:nat]O
+                      | (consn n a (consn m b l)) => [_:nat](plus n m)
+                      end.
+
+
+Type [n:nat]         Cases niln of 
+                         niln  => [_:nat]O
+                      | (consn n a niln) => [_:nat]O
+                      | (consn n a (consn m b l)) => [_:nat](plus n m)
+                      end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+                  <[_:nat]nat->nat>Cases l of 
+                         Niln  => [_:nat]O
+                      | (Consn  n a Niln) =>  [_:nat] n
+                      | (Consn  n a (Consn  m b l)) => [_:nat](plus n m)
+                      end.
+
+Type [A:Set][n:nat][l:(Listn A n)]
+                        Cases l of 
+                         Niln  => [_:nat]O
+                      | (Consn  n a Niln) =>  [_:nat] n
+                      | (Consn  n a (Consn  m b l)) => [_:nat](plus n m)
+                      end.
+
+(* Alsos tests for multiple _ patterns *)
+Type [A:Set][n:nat][l:(Listn A n)]
+                  <[n:nat](Listn A n)>Cases l of 
+                        (Niln as b) => b
+                      | ((Consn _ _ _ ) as b)=>  b
+                      end.
+
+(** Horrible error message! 
+
+Type [A:Set][n:nat][l:(Listn A n)]
+                        Cases l of 
+                        (Niln as b) => b
+                      | ((Consn _ _ _ ) as b)=>  b
+                      end.
+******)
+
+Type   <[n:nat](listn  n)>Cases niln of 
+               (niln as b) => b
+          | ((consn _ _ _ ) as b)=>  b
+          end.
+
+
+Type   <[n:nat](listn  n)>Cases niln of 
+               (niln as b) => b
+          |    x  =>  x
+          end.
+
+Type [n,m:nat][h:(LE n m)]<[_:nat]nat->nat>Cases h  of 
+                         LE_n   => [_:nat]n
+                      | (LE_S  m LE_n) => [_:nat](plus n m)
+                      | (LE_S  m (LE_S y h)) => [_:nat](plus m y )
+                      end.
+Type [n,m:nat][h:(LE n m)]Cases h  of 
+                         LE_n   => [_:nat]n
+                      | (LE_S  m LE_n) => [_:nat](plus n m)
+                      | (LE_S  m (LE_S y h)) => [_:nat](plus m y )
+                      end.
+
+
+Type [n,m:nat][h:(LE n m)]
+    <[_:nat]nat>Cases h  of 
+        LE_n   => n
+      | (LE_S m  LE_n ) => (plus n m)
+      | (LE_S  m (LE_S  y  LE_n )) => (plus (plus n m) y)
+      | (LE_S  m (LE_S  y (LE_S  y' h))) => (plus (plus n m) (plus y y'))
+                      end.
+
+
+
+Type [n,m:nat][h:(LE n m)]
+       Cases h  of 
+        LE_n   => n
+      | (LE_S m  LE_n ) => (plus n m)
+      | (LE_S  m (LE_S  y  LE_n )) => (plus (plus n m) y)
+      | (LE_S  m (LE_S  y (LE_S  y' h))) => (plus (plus n m) (plus y y'))
+                      end.
+
+
+Type [n,m:nat][h:(LE n m)]<[_:nat]nat>Cases h  of 
+                        LE_n   => n
+                      | (LE_S m LE_n) => (plus n m)
+                      | (LE_S  m (LE_S y h)) => (plus (plus n m) y)
+                      end.
+
+
+Type [n,m:nat][h:(LE n m)]Cases h  of 
+                        LE_n   => n
+                      | (LE_S m LE_n) => (plus n m)
+                      | (LE_S  m (LE_S y h)) => (plus (plus n m) y)
+                      end.
+
+Type [n,m:nat]
+                    <[_,_:nat]nat>Cases (LeO O) of 
+                        (LeS n m h)  =>(plus n m)
+                      | x => O
+                      end.
+
+Type [n,m:nat]
+                      Cases (LeO O) of 
+                        (LeS n m h)  =>(plus n m)
+                      | x => O
+                      end.
+
+Parameter test : (n:nat){(le O n)}+{False}.
+Type  [n:nat]<nat>Cases (test n) of
+                        (left _) => O 
+                        | _ => O end.
+
+
+Type  [n:nat]   <nat> Cases (test n) of
+                          (left _) => O 
+                        | _ => O end.
+
+Type  [n:nat]Cases (test n) of
+                          (left _) => O 
+                        | _ => O end.
+
+Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}.
+Type <nat>Cases (compare O O) of
+               (* k<i *)  (inleft (left _)) => O
+            |  (* k=i *)  (inleft  _)  => O
+            |  (* k>i *)  (inright  _) => O end.
+
+Type    Cases (compare O O) of
+               (* k<i *)  (inleft (left _)) => O
+            |  (* k=i *)  (inleft  _)  => O
+            |  (* k>i *)  (inright  _) => O end.
+
+
+
+CoInductive SStream [A:Set]  : (nat->A->Prop)->Set :=
+scons  : 
+  (P:nat->A->Prop)(a:A)(P O a)->(SStream A [n:nat](P (S n)))->(SStream A P).
+Parameter B : Set.
+
+Type 
+  [P:nat->B->Prop][x:(SStream B P)]<[_:nat->B->Prop]B>Cases x of
+     (scons _ a _ _) => a  end.
+
+
+Type 
+  [P:nat->B->Prop][x:(SStream B P)] Cases x of
+     (scons _ a _ _) => a  end.
+
+Type <nat*nat>Cases (O,O) of  (x,y) => ((S x),(S y)) end.
+Type <nat*nat>Cases (O,O) of  ((x as b), y) => ((S x),(S y)) end.
+Type <nat*nat>Cases (O,O) of  (pair x y) => ((S x),(S y)) end.
+
+Type Cases (O,O) of  (x,y) => ((S x),(S y)) end.
+Type Cases (O,O) of  ((x as b), y) => ((S x),(S y)) end.
+Type Cases (O,O) of  (pair x y) => ((S x),(S y)) end.
+
+
+
+Parameter concat : (A:Set)(List A) ->(List A) ->(List A).
+
+Type <(List nat)>Cases (Nil nat) (Nil nat) of 
+                 (Nil as b)  x  => (concat nat b x)
+              | ((Cons _ _) as d) (Nil as c) => (concat nat d c)
+              |  _ _ => (Nil nat)
+              end.
+Type Cases (Nil nat) (Nil nat) of 
+           (Nil as b)  x  => (concat nat b x)
+       | ((Cons _ _) as d) (Nil as c) => (concat nat d c)
+       |  _ _ => (Nil nat)
+       end.
+
+
+Inductive redexes : Set :=
+    VAR : nat -> redexes
+  | Fun : redexes -> redexes
+  | Ap  : bool -> redexes -> redexes -> redexes.
+
+Fixpoint regular [U:redexes] : Prop := <Prop>Cases U of
+  (VAR n) => True
+| (Fun V) => (regular V)
+| (Ap true ((Fun _) as V)  W) => (regular V) /\ (regular W)
+| (Ap true _ W) => False
+| (Ap false V W) => (regular V) /\ (regular W) 
+end.
+
+
+Type [n:nat]Cases n of O => O | (S ((S n) as V)) => V | _ => O end.
+
+Reset concat.
+Parameter concat :(n:nat) (listn n) -> (m:nat) (listn m)-> (listn (plus n m)).
+Type [n:nat][l:(listn n)][m:nat][l':(listn m)] 
+ <[n,_:nat](listn (plus n m))>Cases l l' of 
+                 niln  x => x
+              | (consn n a l'') x =>(consn (plus n m) a (concat n l'' m x))
+               end.
+
+Type [x,y,z:nat]
+        [H:x=y]
+         [H0:y=z]<[_:nat]x=z>Cases H of refl_equal => 
+                          <[n:nat]x=n>Cases H0 of refl_equal => H
+                                             end
+                                       end.
+
+Type [h:False]<False>Cases h of end.
+
+Type [h:False]<True>Cases h of end.
+
+Definition is_zero := [n:nat]Cases n of O => True | _ => False end.
+
+Type [n:nat][h:O=(S n)]<[n:nat](is_zero n)>Cases h of refl_equal => I end.
+
+Definition disc : (n:nat)O=(S n)->False :=
+  [n:nat][h:O=(S n)]
+      <[n:nat](is_zero n)>Cases h of refl_equal => I end.
+
+Definition nlength3 := [n:nat] [l: (listn n)]
+                         Cases l of 
+                            niln  => O
+                         |  (consn O  _ _)  => (S O)
+                         |  (consn (S n)  _ _) => (S (S n))
+                         end.
+
+(* == Testing strategy elimintation predicate  synthesis == *)
+Section titi.
+Variable h:False.
+Type Cases O of 
+          O  => O
+       |  _  => (Except h)
+       end.
+End titi.
+
+Type Cases niln of 
+    (consn _ a niln) => a
+ |  (consn n _ x)    => O
+ |   niln  => O
+ end.
+
+
+
+Inductive wsort : Set := ws : wsort | wt : wsort.
+Inductive TS : wsort->Set := 
+   id :(TS ws) 
+| lift:(TS ws)->(TS ws).
+
+Type [b:wsort][M:(TS b)][N:(TS b)]
+ Cases   M   N of   
+  (lift M1)   id => False 
+ | _ _ => True 
+ end.
+
+
+
+(* ===================================================================== *)
+(* To test pattern matching over a non-dependent inductive type, but     *)
+(* having constructors with some arguments that depend on others         *)
+(* I.e. to test manipulation of elimination predicate                    *)
+(* ===================================================================== *)
+
+
+Parameter LTERM : nat -> Set.
+Mutual Inductive TERM : Type :=
+	  var : TERM
+	| oper : (op:nat) (LTERM op) -> TERM.
+
+Parameter t1, t2:TERM.
+
+Type Cases t1 t2 of 
+   var   var  => True
+
+ | (oper op1 l1)  (oper op2 l2) => False
+ | _ _ => False 
+ end. 
+Reset LTERM.
+
+
+
+Require Peano_dec.
+Parameter n:nat.
+Definition eq_prf := (EXT m | n=m).
+Parameter p:eq_prf .
+
+Type Cases p of
+     (exT_intro c eqc) =>
+          Cases (eq_nat_dec c n) of
+            (right _) => (refl_equal ? n)
+           |(left y) (* c=n*) => (refl_equal ? n) 
+          end
+     end.
+
+
+Parameter ordre_total : nat->nat->Prop.
+
+Parameter N_cla:(N:nat){N=O}+{N=(S O)}+{(ge N (S (S O)))}.
+
+Parameter exist_U2:(N:nat)(ge N (S (S O)))->
+                      {n:nat|(m:nat)(lt O m)/\(le m N)
+                             /\(ordre_total n m)                   
+                             /\(lt O n)/\(lt n N)}.
+
+Type [N:nat](Cases (N_cla N) of
+                         (inright H)=>(Cases (exist_U2 N H) of
+                                               (exist a b)=>a
+                                       end)
+                        |   _       => O
+                       end).
+
+
+
+(* ============================================== *)
+(*     To test compilation of dependent case      *)
+(*  Nested patterns                               *)
+(* ============================================== *)
+
+(* == To test that terms named with AS are correctly absolutized before
+      substitution in rhs   == *)
+
+Type [n:nat]<[n:nat]nat>Cases (n) of 
+          O  => O
+       |  (S O)  => O
+       |  ((S (S n1)) as N)  => N
+      end.
+
+(* ========= *)
+
+Type <[n:nat][_:(listn n)]Prop>Cases niln of 
+                         niln => True
+                       | (consn (S O) _ _) => False
+                       | _ => True end.
+
+Type <[n:nat][_:(listn n)]Prop>Cases niln of 
+                         niln => True
+                       | (consn (S (S O)) _ _) => False
+                       | _ => True end.
+
+
+Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of 
+                         (LeO _) => O
+                       | (LeS (S x) _ _) => x
+                       | _ => (S O) end.
+
+Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of 
+                         (LeO _) => O
+                       | (LeS (S x)  (S y) _) => x
+                       | _ => (S O) end.
+
+Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of 
+                         (LeO _) => O
+                       | (LeS ((S x) as b)  (S y) _) => b
+                       | _ => (S O) end.
+
+
+
+Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m).
+Parameter discr_r : (n:nat) ~(O=(S n)).
+Parameter discr_l : (n:nat) ~((S n)=O).
+
+Type 
+[n:nat] 
+  <[n:nat]n=O\/~n=O>Cases n of 
+      O     => (or_introl ? ~O=O (refl_equal ? O))      
+   |  (S x) => (or_intror (S x)=O ? (discr_l x))
+  end.
+
+
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := 
+[m:nat]
+ <[n,m:nat] n=m \/ ~n=m>Cases n m of
+      O   O   => (or_introl ? ~O=O (refl_equal ? O))
+
+   |  O (S x) => (or_intror O=(S x) ? (discr_r x))
+
+   | (S x) O  => (or_intror ? ~(S x)=O (discr_l x))
+
+   | (S x) (S y) =>  
+      <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of
+        (or_introl h) => (or_introl  ? ~(S x)=(S y) (f_equal nat nat S x y h))
+      | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h))   
+      end
+ end.
+
+Reset eqdec.
+
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := 
+<[n:nat] (m:nat)n=m \/ ~n=m>Cases n  of
+    O  => [m:nat] <[m:nat]O=m\/~O=m>Cases m of 
+                     O    => (or_introl ? ~O=O (refl_equal nat O))
+                   |(S x) => (or_intror O=(S x) ?  (discr_r x))
+                  end
+  | (S x) => [m:nat] 
+    <[m:nat](S x)=m\/~(S x)=m>Cases m of  
+        O    => (or_intror (S x)=O ? (discr_l x))
+     | (S y) =>  
+         <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of
+            (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal ? ? S x y h))
+          | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h))   
+         end
+    end
+ end.
+
+
+Inductive empty : (n:nat)(listn n)-> Prop := 
+  intro_empty: (empty O niln).
+
+Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
+
+Type 
+[n:nat] [l:(listn n)]
+  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
+        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
+   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
+  end.
+
+Reset ff.
+Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m).
+Parameter discr_r : (n:nat) ~(O=(S n)).
+Parameter discr_l : (n:nat) ~((S n)=O).
+
+Type 
+[n:nat] 
+  <[n:nat]n=O\/~n=O>Cases n of 
+      O     => (or_introl ? ~O=O (refl_equal ? O))      
+   |  (S x) => (or_intror (S x)=O ? (discr_l x))
+  end.
+
+
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := 
+[m:nat]
+ <[n,m:nat] n=m \/ ~n=m>Cases n m of
+      O   O   => (or_introl ? ~O=O (refl_equal ? O))
+
+   |  O (S x) => (or_intror O=(S x) ? (discr_r x))
+
+   | (S x) O  => (or_intror ? ~(S x)=O (discr_l x))
+
+   | (S x) (S y) =>  
+      <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of
+        (or_introl h) => (or_introl  ? ~(S x)=(S y) (f_equal nat nat S x y h))
+      | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h))   
+      end
+ end.
+Reset eqdec.
+
+Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := 
+<[n:nat] (m:nat)n=m \/ ~n=m>Cases n  of
+    O  => [m:nat] <[m:nat]O=m\/~O=m>Cases m of 
+                     O    => (or_introl ? ~O=O (refl_equal nat O))
+                   |(S x) => (or_intror O=(S x) ?  (discr_r x))
+                  end
+  | (S x) => [m:nat] 
+    <[m:nat](S x)=m\/~(S x)=m>Cases m of  
+        O    => (or_intror (S x)=O ? (discr_l x))
+     | (S y) =>  
+         <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of
+            (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal ? ? S x y h))
+          | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h))   
+         end
+    end
+ end.
+
+
+(* ================================================== *)
+(* Pour tester parametres                             *)
+(* ================================================== *)
+
+
+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
+  <[l:(List nat)](Empty nat l) \/ ~(Empty nat l)>Cases (Nil nat) of 
+        Nil   =>  (or_introl ? ~(Empty nat (Nil nat)) (intro_Empty nat))
+   |   (Cons a y)  =>  (or_intror (Empty nat (Cons nat a y)) ? 
+                                   (inv_Empty nat a y))
+  end.
+
+
+(* ================================================== *)
+(* Sur les listes                                     *)
+(* ================================================== *)
+
+
+Inductive empty : (n:nat)(listn n)-> Prop := 
+  intro_empty: (empty O niln).
+
+Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)).
+
+Type 
+[n:nat] [l:(listn n)]
+  <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of 
+        niln               =>  (or_introl ? ~(empty O niln) intro_empty)
+   |  ((consn n a y) as b) =>  (or_intror (empty (S n) b) ? (inv_empty n a y))
+  end.
+
+(* ===================================== *)
+(*   Test parametros:                    *)
+(* ===================================== *)
+
+Inductive eqlong : (List nat)-> (List nat)-> Prop :=
+ eql_cons : (n,m:nat)(x,y:(List nat)) 
+            (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y))
+| eql_nil :  (eqlong (Nil nat) (Nil nat)).
+
+
+Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)).
+Parameter V2 : (a:nat)(x:(List nat))
+      (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)).
+Parameter V3 : (a:nat)(x:(List nat))
+      (eqlong  (Cons nat a x)  (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)).
+Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat))
+      (eqlong  (Cons nat a x)(Cons nat b y))
+        \/ ~(eqlong (Cons nat a x) (Cons nat b y)).
+
+Type
+ <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of
+      Nil Nil   => V1
+   |  Nil (Cons a x)  => (V2 a x)
+   |  (Cons a x)  Nil => (V3 a x)
+   | (Cons a x)  (Cons b y)  => (V4 a x b y)
+ end.
+
+
+Type
+[x,y:(List nat)]
+ <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of
+      Nil Nil   => V1
+   |  Nil (Cons a x)  => (V2 a x)
+   |  (Cons a x)  Nil => (V3 a x)
+   | (Cons a x)  (Cons b y)  => (V4 a x b y)
+ end.
+
+ 
+(* ===================================== *)
+
+Inductive Eqlong : (n:nat) (listn n)-> (m:nat) (listn m)-> Prop :=
+ Eql_cons : (n,m:nat )(x:(listn n))(y:(listn m)) (a,b:nat) 
+            (Eqlong n x m y) 
+             ->(Eqlong (S n) (consn n a x) (S m) (consn m b y))
+| Eql_niln :  (Eqlong O niln O niln).
+
+
+Parameter W1 : (Eqlong O niln O niln)\/ ~(Eqlong O niln O niln).
+Parameter W2 : (n,a:nat)(x:(listn n)) 
+  (Eqlong O niln (S n)(consn n a x)) \/ ~(Eqlong  O niln (S n) (consn n a x)).
+Parameter W3 : (n,a:nat)(x:(listn n)) 
+ (Eqlong (S n) (consn n a x)  O niln) \/ ~(Eqlong (S n) (consn n a x)  O niln).
+Parameter W4 : (n,a:nat)(x:(listn n)) (m,b:nat)(y:(listn m)) 
+      (Eqlong  (S n)(consn n a x) (S m) (consn m b y))
+        \/ ~(Eqlong (S n)(consn n a x) (S m) (consn m b y)).
+
+Type
+ <[n:nat][x:(listn n)][m:nat][y:(listn m)]
+     (Eqlong n x m y)\/~(Eqlong n x m y)>Cases niln  niln  of
+      niln niln   => W1
+   |  niln (consn n a x)  => (W2 n a x)
+   |  (consn n a x)  niln => (W3 n a x)
+   | (consn n a x)  (consn m b y)  => (W4 n a x m b y)
+ end.
+
+
+Type 
+[n,m:nat][x:(listn n)][y:(listn m)]
+ <[n:nat][x:(listn n)][m:nat][y:(listn m)]
+     (Eqlong n x m y)\/~(Eqlong n x m y)>Cases x y of
+      niln niln   => W1
+   |  niln (consn n a x)  => (W2 n a x)
+   |  (consn n a x)  niln => (W3 n a x)
+   | (consn n a x)  (consn m b y)  => (W4 n a x m b y)
+ end.
+
+
+Parameter Inv_r : (n,a:nat)(x:(listn n)) ~(Eqlong O niln (S n) (consn n a x)).
+Parameter Inv_l : (n,a:nat)(x:(listn n)) ~(Eqlong (S n) (consn n a x) O niln).
+Parameter Nff : (n,a:nat)(x:(listn n)) (m,b:nat)(y:(listn m)) 
+               ~(Eqlong n x m y)
+                -> ~(Eqlong (S n) (consn n a x) (S m) (consn m b y)).
+
+
+
+Fixpoint Eqlongdec [n:nat; x:(listn n)] : (m:nat)(y:(listn m))
+                                           (Eqlong n x m y)\/~(Eqlong n x m y)
+:= [m:nat][y:(listn m)]
+ <[n:nat][x:(listn n)][m:nat][y:(listn m)]
+     (Eqlong n x m y)\/~(Eqlong n x m y)>Cases x y of
+      niln niln   => (or_introl ? ~(Eqlong O niln O niln)  Eql_niln)
+
+   |  niln ((consn n a x) as L)  => 
+        (or_intror (Eqlong O niln (S n) L)  ? (Inv_r n a x))
+
+   | ((consn n a x) as L)  niln => 
+       (or_intror (Eqlong (S n) L O niln) ? (Inv_l n a x))
+
+
+   | ((consn n a x) as L1) ((consn m b y) as L2) =>
+     <(Eqlong (S n) L1 (S m) L2) \/~(Eqlong (S n) L1 (S m) L2)>
+      Cases (Eqlongdec n x m y) of
+        (or_introl h) => 
+           (or_introl  ? ~(Eqlong (S n) L1 (S m) L2)(Eql_cons n m x y a b h))
+      | (or_intror h) => 
+           (or_intror (Eqlong (S n) L1 (S m) L2) ? (Nff n a x  m b y h))   
+      end
+ end.
+
+(* ============================================== *)
+(*     To test compilation of dependent case      *)
+(*      Multiple Patterns                         *)
+(* ============================================== *)
+Inductive skel: Type :=
+     PROP: skel
+   | PROD: skel->skel->skel.
+
+Parameter Can : skel -> Type.
+Parameter default_can : (s:skel) (Can s).
+
+Type  [s1,s2:skel]
+[s1,s2:skel]<[s1:skel][_:skel](Can s1)>Cases s1 s2 of
+  PROP PROP => (default_can PROP)
+| (PROD x y) PROP => (default_can (PROD x y))
+| (PROD x y) _ => (default_can (PROD x y))
+| PROP _ => (default_can PROP)
+end.
+
+(* to test bindings in nested Cases *)
+(* ================================ *)
+Inductive Pair : Set :=
+  pnil : Pair |
+  pcons : Pair -> Pair -> Pair.
+
+Type [p,q:Pair]Cases p of
+  (pcons _ x) => 
+     Cases q of 
+      (pcons _ (pcons _ x)) => True
+     |  _  => False
+     end
+|  _  => False
+end.
+
+
+Type [p,q:Pair]Cases p of
+  (pcons _ x) => 
+     Cases q of 
+      (pcons _ (pcons _ x)) => 
+          Cases q of 
+              (pcons _ (pcons _ (pcons _ x))) => x
+           | _ => pnil
+           end
+     |  _  => pnil
+     end
+|  _  => pnil
+end.
+
+Type  
+  [n:nat]
+         [l:(listn (S n))]
+           <[z:nat](listn (pred z))>Cases l of 
+                       niln  => niln
+                    |  (consn n _ l)  => 
+                           <[m:nat](listn m)>Cases l of 
+                                             niln => niln
+                                           | b => b
+                                           end
+                   end.
+
+
+
+(* Test de la syntaxe avec nombres *)
+Require Arith.
+Type [n]Cases n of 2 => true | _ => false end.
+
+Require ZArith.
+Type [n]Cases n of `0` => true | _ => false end.
diff --git a/test-suite/ideal-features/CasesDep.v b/test-suite/ideal-features/CasesDep.v
new file mode 100644
index 000000000..3a0c36b6d
--- /dev/null
+++ b/test-suite/ideal-features/CasesDep.v
@@ -0,0 +1,374 @@
+
+(* -------------------------------------------------------------------- *)
+(*   Example to test patterns matching on dependent families            *)     (* This exemple extracted from the developement done by Nacira Chabane  *)
+(* (equipe Paris 6)                                                     *)
+(* -------------------------------------------------------------------- *)
+
+
+Require Prelude.
+Require Logic_TypeSyntax.
+Require Logic_Type.
+
+
+Section Orderings.
+   Variable U: Type.
+   
+   Definition Relation :=  U -> U -> Prop.
+
+   Variable R: Relation.
+   
+   Definition Reflexive : Prop :=  (x: U) (R x x).
+   
+   Definition Transitive : Prop :=  (x,y,z: U) (R x y) -> (R y z) -> (R x z).
+   
+   Definition Symmetric : Prop :=  (x,y: U) (R x y) -> (R y x).
+   
+   Definition Antisymmetric : Prop :=
+      (x,y: U) (R x y) -> (R y x) -> x==y.
+   
+   Definition contains : Relation -> Relation -> Prop :=
+      [R,R': Relation] (x,y: U) (R' x y) -> (R x y).
+  Definition same_relation : Relation -> Relation -> Prop :=
+      [R,R': Relation] (contains R R') /\ (contains R' R).
+Inductive Equivalence : Prop :=
+         Build_Equivalence:
+           Reflexive -> Transitive -> Symmetric -> Equivalence.
+   
+   Inductive PER : Prop :=
+         Build_PER: Symmetric -> Transitive -> PER.
+   
+End Orderings.
+
+(***** Setoid  *******)
+
+Inductive Setoid : Type 
+  := Build_Setoid : (S:Type)(R:(Relation S))(Equivalence ? R) -> Setoid.
+
+Definition elem := [A:Setoid] let (S,R,e)=A in S.
+
+Grammar command command1 :=
+ elem  [ "|" command0($s) "|"] -> [ <<(elem $s)>>].
+
+Definition equal := [A:Setoid]
+   <[s:Setoid](Relation |s|)>let (S,R,e)=A in R.
+
+Grammar command command1 :=
+ equal   [ command0($c) "=" "%" "S" command0($c2) ] -> 
+         [ <<(equal ? $c $c2)>>].
+
+
+Axiom prf_equiv : (A:Setoid)(Equivalence |A| (equal A)).
+Axiom prf_refl : (A:Setoid)(Reflexive |A| (equal A)).
+Axiom prf_sym : (A:Setoid)(Symmetric |A| (equal A)).
+Axiom prf_trans : (A:Setoid)(Transitive |A| (equal A)).
+
+Section Maps.
+Variables A,B: Setoid.
+
+Definition Map_law := [f:|A| -> |B|]
+    (x,y:|A|) x =%S y -> (f x) =%S (f y).
+
+Inductive Map : Type :=
+    Build_Map : (f:|A| -> |B|)(p:(Map_law f))Map.
+
+Definition explicit_ap := [m:Map] <|A| -> |B|>Match m with 
+         [f:?][p:?]f end.
+
+Axiom pres : (m:Map)(Map_law (explicit_ap m)).
+
+Definition ext := [f,g:Map]
+         (x:|A|) (explicit_ap f x) =%S (explicit_ap g x).
+
+Axiom Equiv_map_eq : (Equivalence Map ext).
+
+Definition Map_setoid := (Build_Setoid Map ext Equiv_map_eq).
+
+End Maps.
+
+Syntactic Definition ap := (explicit_ap ? ?). 
+
+Grammar command command8 :=
+  map_setoid [ command7($c1) "=>" command8($c2) ] 
+                 -> [ <<(Map_setoid $c1 $c2)>>].
+
+
+Definition ap2 := [A,B,C:Setoid][f:|(A=>(B=>C))|][a:|A|] (ap (ap f a)).
+
+
+(*****    posint     ******)
+
+Inductive posint : Type
+        := Z : posint | Suc : posint -> posint.
+
+Require Logic_Type.
+
+Axiom f_equal : (A,B:Type)(f:A->B)(x,y:A) x==y -> (f x)==(f y).
+Axiom eq_Suc : (n,m:posint) n==m -> (Suc n)==(Suc m).
+
+(* The predecessor function *)
+
+Definition pred : posint->posint
+     := [n:posint](<posint>Case n of (* Z *) Z 
+                            (* Suc u *) [u:posint]u end).
+
+Axiom pred_Sucn : (m:posint) m==(pred (Suc m)).
+Axiom eq_add_Suc : (n,m:posint) (Suc n)==(Suc m) -> n==m.
+Axiom not_eq_Suc : (n,m:posint) ~(n==m) -> ~((Suc n)==(Suc m)).
+
+
+Definition IsSuc : posint->Prop
+  := [n:posint](<Prop>Case n of (* Z *) False
+                          (* Suc p *) [p:posint]True end).
+Definition IsZero :posint->Prop :=
+	[n:posint]<Prop>Match n with 
+		True
+		[p:posint][H:Prop]False end.
+
+Axiom Z_Suc : (n:posint) ~(Z==(Suc n)).
+Axiom  Suc_Z: (n:posint) ~(Suc n)==Z.
+Axiom n_Sucn : (n:posint) ~(n==(Suc n)).
+Axiom Sucn_n : (n:posint) ~(Suc n)==n.
+Axiom eqT_symt : (a,b:posint) ~(a==b)->~(b==a).
+
+
+(*******  Dsetoid *****)
+
+Definition Decidable :=[A:Type][R:(Relation A)]
+		(x,y:A)(R x y) \/ ~(R x y).
+
+
+Record DSetoid : Type :=
+{Set_of : Setoid;
+ prf_decid : (Decidable |Set_of| (equal Set_of))}.
+
+(* example de Dsetoide d'entiers *)
+
+
+Axiom eqT_equiv : (Equivalence posint (eqT posint)).
+Axiom Eq_posint_deci : (Decidable posint (eqT posint)).
+
+(* Dsetoide des posint*)
+
+Definition Set_of_posint := (Build_Setoid posint (eqT posint) eqT_equiv).
+
+Definition Dposint := (Build_DSetoid Set_of_posint Eq_posint_deci).
+
+
+
+(**************************************)
+
+
+(* Definition des signatures *)
+(* une signature est un ensemble d'operateurs muni
+ de l'arite de chaque operateur *)
+
+
+Section Sig.
+
+Record Signature :Type :=
+{Sigma : DSetoid; 
+ Arity : (Map (Set_of Sigma) (Set_of Dposint))}.
+
+Variable S:Signature.
+
+
+
+Variable Var : DSetoid.
+
+Mutual Inductive TERM : Type :=
+	  var : |(Set_of Var)| -> TERM
+	| oper : (op: |(Set_of (Sigma S))| ) (LTERM (ap (Arity S) op)) -> TERM
+with
+	LTERM : posint -> Type :=
+	  nil : (LTERM Z)
+	| cons : TERM -> (n:posint)(LTERM n) -> (LTERM (Suc n)).
+
+
+
+(* -------------------------------------------------------------------- *)
+(*                  Examples                                            *)
+(* -------------------------------------------------------------------- *)
+
+
+Parameter t1,t2: TERM.
+
+Type 
+ Cases t1 t2 of 
+   (var  v1) (var v2) => True
+
+ | (oper op1 l1)  (oper op2 l2) => False
+ | _ _ => False 
+ end.
+
+
+
+Parameter n2:posint.
+Parameter l1, l2:(LTERM n2).
+
+Type 
+ Cases l1 l2  of
+    nil            nil => True 
+ |  (cons v m y)   nil => False
+ |  _               _  => False
+end.
+
+
+Type Cases l1 l2 of
+    nil              nil      => True 
+ | (cons u n x)  (cons v m y) =>False
+ |   _               _        => False
+end.
+
+
+
+Fixpoint equalT [t1:TERM]:TERM->Prop :=
+[t2:TERM] 
+ Cases t1 t2 of 
+   (var  v1)        (var v2)    => True
+ | (oper op1 l1)  (oper op2 l2) => False
+ |  _                   _       => False 
+ end
+
+with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+[n2:posint][l2:(LTERM n2)]
+ Cases l1 l2 of
+    nil                 nil             => True 
+ | (cons t1 n1' l1')  (cons t2 n2' l2') => False
+ | _                    _               => False
+end.
+
+
+Reset equalT.
+Reset EqListT.
+(* ------------------------------------------------------------------*)
+(*          Initial exemple (without patterns)                       *)
+(*-------------------------------------------------------------------*)
+
+Fixpoint equalT [t1:TERM]:TERM->Prop :=
+<TERM->Prop>Case t1 of 
+	(*var*) [v1:|(Set_of Var)|][t2:TERM]
+		<Prop>Case t2 of
+		(*var*)[v2:|(Set_of Var)|] (v1 =%S v2)
+		(*oper*)[op2:|(Set_of (Sigma S))|][_:(LTERM (ap (Arity S) op2))]False
+		end
+	(*oper*)[op1:|(Set_of (Sigma S))|]
+                [l1:(LTERM (ap (Arity S) op1))][t2:TERM]
+                <Prop>Case t2 of
+		(*var*)[v2:|(Set_of Var)|]False
+		(*oper*)[op2:|(Set_of (Sigma S))|]
+                        [l2:(LTERM (ap (Arity S) op2))]
+			((op1=%S op2)/\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2))
+		end
+end
+with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+<[_:posint](n2:posint)(LTERM n2)->Prop>Case l1 of
+	(*nil*) [n2:posint][l2:(LTERM n2)]
+		<[_:posint]Prop>Case l2 of
+		(*nil*)True
+	 	(*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')]False
+	end
+	(*cons*)[t1:TERM][n1':posint][l1':(LTERM n1')]
+		[n2:posint][l2:(LTERM n2)]
+		<[_:posint]Prop>Case l2 of
+		(*nil*) False
+		(*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')]
+			((equalT t1 t2) /\ (EqListT n1' l1' n2' l2'))
+		end
+end.
+
+
+(* ---------------------------------------------------------------- *)
+(*                Version with simple patterns                      *)
+(* ---------------------------------------------------------------- *)
+Reset equalT.
+
+Fixpoint equalT [t1:TERM]:TERM->Prop :=
+Cases t1 of 
+  (var  v1) => [t2:TERM]
+	        Cases t2 of
+		     (var v2) => (v1 =%S v2)
+		 | (oper op2 _) =>False
+		 end
+| (oper op1 l1) => [t2:TERM]
+		    Cases t2 of
+	              (var _) => False
+                    | (oper op2 l2) => (op1=%S op2)
+                      /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)
+		    end
+end
+with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+<[_:posint](n2:posint)(LTERM n2)->Prop>Cases l1 of
+  nil => [n2:posint][l2:(LTERM n2)]
+          Cases l2 of
+              nil => True
+	  | _  => False
+	  end
+| (cons t1 n1' l1') => [n2:posint][l2:(LTERM n2)]
+		        Cases l2 of
+		           nil =>False
+		        | (cons t2 n2' l2') => (equalT t1 t2) 
+                                                /\ (EqListT n1' l1' n2' l2')
+		end
+end.
+
+
+Reset equalT.
+
+Fixpoint equalT [t1:TERM]:TERM->Prop :=
+Cases t1 of 
+  (var  v1) => [t2:TERM]
+	        Cases t2 of
+		     (var v2) => (v1 =%S v2)
+		 | (oper op2 _) =>False
+		 end
+| (oper op1 l1) => [t2:TERM]
+		    Cases t2 of
+	              (var _) => False
+                    | (oper op2 l2) => (op1=%S op2)
+                      /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)
+		    end
+end
+with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+[n2:posint][l2:(LTERM n2)]
+Cases l1 of
+  nil => 
+          Cases l2 of
+              nil => True
+	  | _  => False
+	  end
+| (cons t1 n1' l1') =>  Cases l2 of
+		           nil =>False
+		        | (cons t2 n2' l2') => (equalT t1 t2) 
+                                                /\ (EqListT n1' l1' n2' l2')
+		end
+end.
+
+(* ---------------------------------------------------------------- *)
+(*                  Version with multiple patterns                  *)
+(* ---------------------------------------------------------------- *)
+Reset equalT.
+
+Fixpoint equalT [t1:TERM]:TERM->Prop :=
+[t2:TERM] 
+ Cases t1 t2 of 
+   (var  v1)       (var v2)     => (v1 =%S v2)
+
+ | (oper op1 l1)  (oper op2 l2) => 
+     (op1=%S op2) /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)
+
+ |  _               _ => False 
+ end
+
+with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+[n2:posint][l2:(LTERM n2)]
+ Cases l1 l2 of
+    nil                nil              => True 
+ | (cons t1 n1' l1')  (cons t2 n2' l2') => (equalT t1 t2) 
+                                          /\ (EqListT n1' l1' n2'  l2')
+ | _ _ => False
+end.
+
+
+(* ------------------------------------------------------------------ *)
+
+End Sig.