Imported Upstream snapshot 8.3~beta0+13298

10 files changed, 1174 insertions, 1443 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index c015854e..f42dc7fa 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: List.v 12446 2009-10-29 21:43:06Z glondu $ i*)
+(*i $Id$ i*)
 
 Require Import Le Gt Minus Min Bool.
 
@@ -17,78 +17,47 @@ Set Implicit Arguments.
 (** * Basics: definition of polymorphic lists and some operations *)
 (******************************************************************)
 
-(** ** Definitions *)
+(** The definition of [list] is now in [Init/Datatypes],
+    as well as the definitions of [length] and [app] *)
+
+Open Scope list_scope.
 
 Section Lists.
 
   Variable A : Type.
 
-  Inductive list : Type :=
-    | nil : list
-    | cons : A -> list -> list.
-
-  Infix "::" := cons (at level 60, right associativity) : list_scope.
+  (** Head and tail *)
 
-  Open Scope list_scope.
+  Definition hd (default:A) (l:list A) :=
+    match l with
+      | nil => default
+      | x :: _ => x
+    end.
 
-  (** Head and tail        *)
-  Definition head (l:list) :=
+  Definition hd_error (l:list A) :=
     match l with
       | nil => error
       | x :: _ => value x
     end.
 
- Definition hd (default:A) (l:list) :=
-   match l with
-     | nil => default
-     | x :: _ => x
-   end. 
-
-  Definition tail (l:list) : list :=
+  Definition tl (l:list A) :=
     match l with
       | nil => nil
       | a :: m => m
     end.
 
-  (** Length of lists                *)
-  Fixpoint length (l:list) : nat :=
-    match l with
-      | nil => 0
-      | _ :: m => S (length m)
-    end.
-
   (** The [In] predicate *)
-  Fixpoint In (a:A) (l:list) {struct l} : Prop :=
+  Fixpoint In (a:A) (l:list A) : Prop :=
     match l with
       | nil => False
       | b :: m => b = a \/ In a m
     end.
 
-
-  (** Concatenation of two lists *)
-  Fixpoint app (l m:list) {struct l} : list :=
-    match l with
-      | nil => m
-      | a :: l1 => a :: app l1 m
-    end.
-  
-  Infix "++" := app (right associativity, at level 60) : list_scope.
-  
 End Lists.
 
-(** Exporting list notations and tactics *)
-
-Implicit Arguments nil [A].
-Infix "::" := cons (at level 60, right associativity) : list_scope.
-Infix "++" := app (right associativity, at level 60) : list_scope.
-
-Open Scope list_scope.
-
-Delimit Scope list_scope with list.
-
-Bind Scope list_scope with list.
-
-Arguments Scope list [type_scope].
+(* Keep these notations local to prevent conflicting notations *)
+Local Notation "[ ]" := nil : list_scope.
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
 
 (** ** Facts about lists *)
 
@@ -100,164 +69,172 @@ Section Facts.
   (** *** Genereric facts *)
 
   (** Discrimination *)
-  Theorem nil_cons : forall (x:A) (l:list A), nil <> x :: l.
-  Proof. 
+  Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l.
+  Proof.
     intros; discriminate.
   Qed.
 
 
   (** Destruction *)
 
-  Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = nil}.
+  Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = []}.
   Proof.
-    induction l as [|a tl].
+    induction l as [|a tail].
     right; reflexivity.
-    left; exists a; exists tl; reflexivity.
+    left; exists a, tail; reflexivity.
   Qed.
-    
+
   (** *** Head and tail *)
-  
-  Theorem head_nil : head (@nil A) = None.
+
+  Theorem hd_error_nil : hd_error (@nil A) = None.
   Proof.
     simpl; reflexivity.
   Qed.
 
-  Theorem head_cons : forall (l : list A) (x : A), head (x::l) = Some x.
+  Theorem hd_error_cons : forall (l : list A) (x : A), hd_error (x::l) = Some x.
   Proof.
     intros; simpl; reflexivity.
   Qed.
 
 
   (************************)
-  (** *** Facts about [In] *) 
+  (** *** Facts about [In] *)
   (************************)
 
 
   (** Characterization of [In] *)
-  
+
   Theorem in_eq : forall (a:A) (l:list A), In a (a :: l).
-  Proof. 
-    simpl in |- *; auto.
+  Proof.
+    simpl; auto.
   Qed.
-  
+
   Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l).
-  Proof. 
-    simpl in |- *; auto.
+  Proof.
+    simpl; auto.
   Qed.
 
-  Theorem in_nil : forall a:A, ~ In a nil.
+  Theorem in_nil : forall a:A, ~ In a [].
   Proof.
-    unfold not in |- *; intros a H; inversion_clear H.
+    unfold not; intros a H; inversion_clear H.
   Qed.
 
-  Lemma In_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2.
+  Theorem in_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2.
   Proof.
   induction l; simpl; destruct 1.
   subst a; auto.
-  exists (@nil A); exists l; auto.
+  exists [], l; auto.
   destruct (IHl H) as (l1,(l2,H0)).
-  exists (a::l1); exists l2; simpl; f_equal; auto.
+  exists (a::l1), l2; simpl; f_equal; auto.
   Qed.
 
   (** Inversion *)
-  Theorem in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l.
+  Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l.
   Proof.
     intros a b l H; inversion_clear H; auto.
   Qed.
 
   (** Decidability of [In] *)
-  Theorem In_dec :
+  Theorem in_dec :
     (forall x y:A, {x = y} + {x <> y}) ->
     forall (a:A) (l:list A), {In a l} + {~ In a l}.
   Proof.
     intro H; induction l as [| a0 l IHl].
     right; apply in_nil.
-    destruct (H a0 a); simpl in |- *; auto.
-    destruct IHl; simpl in |- *; auto. 
-    right; unfold not in |- *; intros [Hc1| Hc2]; auto.
+    destruct (H a0 a); simpl; auto.
+    destruct IHl; simpl; auto.
+    right; unfold not; intros [Hc1| Hc2]; auto.
   Defined.
 
 
-  (*************************)
+  (**************************)
   (** *** Facts about [app] *)
-  (*************************)
+  (**************************)
 
   (** Discrimination *)
-  Theorem app_cons_not_nil : forall (x y:list A) (a:A), nil <> x ++ a :: y.
+  Theorem app_cons_not_nil : forall (x y:list A) (a:A), [] <> x ++ a :: y.
   Proof.
-    unfold not in |- *.
-    destruct x as [| a l]; simpl in |- *; intros.
+    unfold not.
+    destruct x as [| a l]; simpl; intros.
     discriminate H.
     discriminate H.
   Qed.
 
 
   (** Concat with [nil] *)
+  Theorem app_nil_l : forall l:list A, [] ++ l = l.
+  Proof.
+    reflexivity.
+  Qed.
 
-  Theorem app_nil_end : forall l:list A, l = l ++ nil.
-  Proof. 
-    induction l; simpl in |- *; auto.
-    rewrite <- IHl; auto.
+  Theorem app_nil_r : forall l:list A, l ++ [] = l.
+  Proof.
+    induction l; simpl; f_equal; auto.
   Qed.
 
+  (* begin hide *)
+  (* Deprecated *)
+  Theorem app_nil_end : forall (l:list A), l = l ++ [].
+  Proof. symmetry; apply app_nil_r. Qed.
+  (* end hide *)
+
   (** [app] is associative *)
-  Theorem app_ass : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n.
-  Proof. 
-    intros. induction l; simpl in |- *; auto.
-    now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n).
-    rewrite <- IHl; auto.
+  Theorem app_assoc : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n.
+  Proof.
+    intros l m n; induction l; simpl; f_equal; auto.
   Qed.
-  Hint Resolve app_ass.
 
-  Theorem ass_app : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n.
-  Proof. 
-    auto using app_ass.
+  (* begin hide *)
+  (* Deprecated *)
+  Theorem app_assoc_reverse : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n.
+  Proof.
+     auto using app_assoc.
   Qed.
+  Hint Resolve app_assoc_reverse.
+  (* end hide *)
 
-  (** [app] commutes with [cons] *) 
+  (** [app] commutes with [cons] *)
   Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y.
   Proof.
     auto.
   Qed.
 
+  (** Facts deduced from the result of a concatenation *)
 
-
-  (** Facts deduced from the result of a concatenation *)  
-
-  Theorem app_eq_nil : forall l l':list A, l ++ l' = nil -> l = nil /\ l' = nil.
+  Theorem app_eq_nil : forall l l':list A, l ++ l' = [] -> l = [] /\ l' = [].
   Proof.
-    destruct l as [| x l]; destruct l' as [| y l']; simpl in |- *; auto.
+    destruct l as [| x l]; destruct l' as [| y l']; simpl; auto.
     intro; discriminate.
     intros H; discriminate H.
   Qed.
 
   Theorem app_eq_unit :
     forall (x y:list A) (a:A),
-      x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil.
+      x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = [].
   Proof.
     destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
-      simpl in |- *.
+      simpl.
     intros a H; discriminate H.
     left; split; auto.
     right; split; auto.
     generalize H.
-    generalize (app_nil_end l); intros E.
-    rewrite <- E; auto.
+    generalize (app_nil_r l); intros E.
+    rewrite -> E; auto.
     intros.
     injection H.
     intro.
-    cut (nil = l ++ a0 :: l0); auto.
+    cut ([] = l ++ a0 :: l0); auto.
     intro.
     generalize (app_cons_not_nil _ _ _ H1); intro.
     elim H2.
   Qed.
 
   Lemma app_inj_tail :
-    forall (x y:list A) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b.
+    forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b.
   Proof.
     induction x as [| x l IHl];
-      [ destruct y as [| a l] | destruct y as [| a l0] ]; 
-      simpl in |- *; auto.
+      [ destruct y as [| a l] | destruct y as [| a l0] ];
+      simpl; auto.
     intros a b H.
     injection H.
     auto.
@@ -266,12 +243,12 @@ Section Facts.
     generalize (app_cons_not_nil _ _ _ H0); destruct 1.
     intros a b H.
     injection H; intros.
-    cut (nil = l ++ a :: nil); auto.
+    cut ([] = l ++ [a]); auto.
     intro.
     generalize (app_cons_not_nil _ _ _ H2); destruct 1.
     intros a0 b H.
     injection H; intros.
-    destruct (IHl l0 a0 b H0). 
+    destruct (IHl l0 a0 b H0).
     split; auto.
     rewrite <- H1; rewrite <- H2; reflexivity.
   Qed.
@@ -285,9 +262,9 @@ Section Facts.
   Qed.
 
   Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m.
-  Proof. 
+  Proof.
     intros l m a.
-    elim l; simpl in |- *; auto.
+    elim l; simpl; auto.
     intros a0 y H H0.
     now_show ((a0 = a \/ In a y) \/ In a m).
     elim H0; auto.
@@ -297,9 +274,9 @@ Section Facts.
   Qed.
 
   Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m).
-  Proof. 
+  Proof.
     intros l m a.
-    elim l; simpl in |- *; intro H.
+    elim l; simpl; intro H.
     now_show (In a m).
     elim H; auto; intro H0.
     now_show (In a m).
@@ -311,18 +288,23 @@ Section Facts.
     now_show (H = a \/ In a (y ++ m)).
     elim H2; auto.
   Qed.
-  
+
+  Lemma in_app_iff : forall l l' (a:A), In a (l++l') <-> In a l \/ In a l'.
+  Proof.
+    split; auto using in_app_or, in_or_app.
+  Qed.
+
   Lemma app_inv_head:
-   forall l l1 l2 : list A, l ++ l1 = l ++ l2 ->  l1 = l2.
+   forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2.
   Proof.
     induction l; simpl; auto; injection 1; auto.
   Qed.
- 
+
   Lemma app_inv_tail:
-    forall l l1 l2 : list A, l1 ++ l = l2 ++ l ->  l1 = l2.
+    forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2.
   Proof.
     intros l l1 l2; revert l1 l2 l.
-    induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; 
+    induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2];
      simpl; auto; intros l H.
     absurd (length (x2 :: l2 ++ l) <= length l).
     simpl; rewrite app_length; auto with arith.
@@ -335,10 +317,10 @@ Section Facts.
 
 End Facts.
 
-Hint Resolve app_nil_end ass_app app_ass: datatypes v62.
+Hint Resolve app_assoc app_assoc_reverse: datatypes v62.
 Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62.
 Hint Immediate app_eq_nil: datatypes v62.
-Hint Resolve app_eq_unit app_inj_tail: datatypes v62. 
+Hint Resolve app_eq_unit app_inj_tail: datatypes v62.
 Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62.
 
 
@@ -359,7 +341,7 @@ Section Elts.
     match n, l with
       | O, x :: l' => x
       | O, other => default
-      | S m, nil => default
+      | S m, [] => default
       | S m, x :: t => nth m t default
     end.
 
@@ -367,26 +349,26 @@ Section Elts.
     match n, l with
       | O, x :: l' => true
       | O, other => false
-      | S m, nil => false
+      | S m, [] => false
       | S m, x :: t => nth_ok m t default
     end.
 
   Lemma nth_in_or_default :
     forall (n:nat) (l:list A) (d:A), {In (nth n l d) l} + {nth n l d = d}.
   (* Realizer nth_ok. Program_all. *)
-  Proof. 
+  Proof.
     intros n l d; generalize n; induction l; intro n0.
     right; case n0; trivial.
-    case n0; simpl in |- *.
+    case n0; simpl.
     auto.
-    intro n1; elim (IHl n1); auto.     
+    intro n1; elim (IHl n1); auto.
   Qed.
 
   Lemma nth_S_cons :
     forall (n:nat) (l:list A) (d a:A),
       In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l).
-  Proof. 
-    simpl in |- *; auto.
+  Proof.
+    simpl; auto.
   Qed.
 
   Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A :=
@@ -402,13 +384,19 @@ Section Elts.
       | None => default
     end.
 
+  Lemma nth_default_eq :
+    forall n l (d:A), nth_default d l n = nth n l d.
+  Proof.
+    unfold nth_default; induction n; intros [ | ] ?; simpl; auto.
+  Qed.
+
   Lemma nth_In :
     forall (n:nat) (l:list A) (d:A), n < length l -> In (nth n l d) l.
 
   Proof.
-    unfold lt in |- *; induction n as [| n hn]; simpl in |- *.
-    destruct l; simpl in |- *; [ inversion 2 | auto ].
-    destruct l as [| a l hl]; simpl in |- *.
+    unfold lt; induction n as [| n hn]; simpl.
+    destruct l; simpl; [ inversion 2 | auto ].
+    destruct l as [| a l hl]; simpl.
     inversion 2.
     intros d ie; right; apply hn; auto with arith.
   Qed.
@@ -420,7 +408,7 @@ Section Elts.
     apply IHl; auto with arith.
   Qed.
 
-  Lemma nth_indep : 
+  Lemma nth_indep :
     forall l n d d', n < length l -> nth n l d = nth n l d'.
   Proof.
     induction l; simpl; intros; auto.
@@ -428,7 +416,7 @@ Section Elts.
     destruct n; simpl; auto with arith.
   Qed.
 
-  Lemma app_nth1 : 
+  Lemma app_nth1 :
     forall l l' d n, n < length l -> nth n (l++l') d = nth n l d.
   Proof.
     induction l.
@@ -439,7 +427,7 @@ Section Elts.
     intros; rewrite IHl; auto with arith.
   Qed.
 
-  Lemma app_nth2 : 
+  Lemma app_nth2 :
     forall l l' d n, n >= length l -> nth n (l++l') d = nth (n-length l) l' d.
   Proof.
     induction l.
@@ -461,53 +449,49 @@ Section Elts.
   (** ** Remove    *)
   (*****************)
 
-  Section Remove.
+  Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
 
-    Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
-    
-    Fixpoint remove (x : A) (l : list A){struct l} : list A :=
-      match l with
-	| nil => nil
-	| y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
-      end.
-    
-    Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).
-    Proof.
-      induction l as [|x l]; auto.
-      intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. 
-      apply IHl.
-      unfold not; intro HF; simpl in HF; destruct HF; auto.
-      apply (IHl y); assumption. 
-    Qed.
-  
-  End Remove.
+  Fixpoint remove (x : A) (l : list A) : list A :=
+    match l with
+      | [] => []
+      | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
+    end.
+
+  Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).
+  Proof.
+    induction l as [|x l]; auto.
+    intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx].
+    apply IHl.
+    unfold not; intro HF; simpl in HF; destruct HF; auto.
+    apply (IHl y); assumption.
+  Qed.
 
 
 (******************************)
 (** ** Last element of a list *)
 (******************************)
 
-  (** [last l d] returns the last element of the list [l], 
+  (** [last l d] returns the last element of the list [l],
     or the default value [d] if [l] is empty. *)
 
-  Fixpoint last (l:list A) (d:A)  {struct l} : A := 
-  match l with 
-    | nil => d 
-    | a :: nil => a 
+  Fixpoint last (l:list A) (d:A) : A :=
+  match l with
+    | [] => d
+    | [a] => a
     | a :: l => last l d
   end.
 
   (** [removelast l] remove the last element of [l] *)
 
-  Fixpoint removelast (l:list A) {struct l} : list A := 
-    match l with 
-      | nil =>  nil 
-      | a :: nil => nil 
+  Fixpoint removelast (l:list A) : list A :=
+    match l with
+      | [] =>  []
+      | [a] => []
       | a :: l => a :: removelast l
     end.
-  
-  Lemma app_removelast_last : 
-    forall l d, l<>nil -> l = removelast l ++ (last l d :: nil).
+
+  Lemma app_removelast_last :
+    forall l d, l <> [] -> l = removelast l ++ [last l d].
   Proof.
     induction l.
     destruct 1; auto.
@@ -515,27 +499,27 @@ Section Elts.
     destruct l; auto.
     pattern (a0::l) at 1; rewrite IHl with d; auto; discriminate.
   Qed.
-  
-  Lemma exists_last : 
-    forall l, l<>nil -> { l' : (list A) & { a : A | l = l'++a::nil}}. 
-  Proof. 
+
+  Lemma exists_last :
+    forall l, l <> [] -> { l' : (list A) & { a : A | l = l' ++ [a]}}.
+  Proof.
     induction l.
     destruct 1; auto.
     intros _.
     destruct l.
-    exists (@nil A); exists a; auto.
+    exists [], a; auto.
     destruct IHl as [l' (a',H)]; try discriminate.
     rewrite H.
-    exists (a::l'); exists a'; auto.
+    exists (a::l'), a'; auto.
   Qed.
 
-  Lemma removelast_app : 
-    forall l l', l' <> nil -> removelast (l++l') = l ++ removelast l'.
+  Lemma removelast_app :
+    forall l l', l' <> [] -> removelast (l++l') = l ++ removelast l'.
   Proof.
     induction l.
     simpl; auto.
     simpl; intros.
-    assert (l++l' <> nil).
+    assert (l++l' <> []).
     destruct l.
     simpl; auto.
     simpl; discriminate.
@@ -543,32 +527,30 @@ Section Elts.
     destruct (l++l'); [elim H0; auto|f_equal; auto].
   Qed.
 
-  
+
   (****************************************)
   (** ** Counting occurences of a element *)
   (****************************************)
 
-  Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}.
-  
-  Fixpoint count_occ (l : list A) (x : A){struct l} : nat :=
-    match l with 
-      | nil => 0
-      | y :: tl => 
-	let n := count_occ tl x in 
-	  if eqA_dec y x then S n else n
+  Fixpoint count_occ (l : list A) (x : A) : nat :=
+    match l with
+      | [] => 0
+      | y :: tl =>
+	let n := count_occ tl x in
+	  if eq_dec y x then S n else n
     end.
-  
+
   (** Compatibility of count_occ with operations on list *)
   Theorem count_occ_In : forall (l : list A) (x : A), In x l <-> count_occ l x > 0.
   Proof.
     induction l as [|y l].
     simpl; intros; split; [destruct 1 | apply gt_irrefl].
-    simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
-    rewrite Heq; intuition. 
+    simpl. intro x; destruct (eq_dec y x) as [Heq|Hneq].
+    rewrite Heq; intuition.
     pose (IHl x). intuition.
   Qed.
-  
-  Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil.
+
+  Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = [].
   Proof.
     split.
     (* Case -> *)
@@ -578,14 +560,14 @@ Section Elts.
     elim (O_S (count_occ l x)).
     apply sym_eq.
     generalize (H x).
-    simpl. destruct (eqA_dec x x) as [|HF].
+    simpl. destruct (eq_dec x x) as [|HF].
     trivial.
     elim HF; reflexivity.
     (* Case <- *)
     intro H; rewrite H; simpl; reflexivity.
   Qed.
-  
-  Lemma count_occ_nil : forall (x : A), count_occ nil x = 0.
+
+  Lemma count_occ_nil : forall (x : A), count_occ [] x = 0.
   Proof.
     intro x; simpl; reflexivity.
   Qed.
@@ -593,13 +575,13 @@ Section Elts.
   Lemma count_occ_cons_eq : forall (l : list A) (x y : A), x = y -> count_occ (x::l) y = S (count_occ l y).
   Proof.
     intros l x y H; simpl.
-    destruct (eqA_dec x y); [reflexivity | contradiction].
+    destruct (eq_dec x y); [reflexivity | contradiction].
   Qed.
-  
+
   Lemma count_occ_cons_neq : forall (l : list A) (x y : A), x <> y -> count_occ (x::l) y = count_occ l y.
   Proof.
     intros l x y H; simpl.
-    destruct (eqA_dec x y); [contradiction | reflexivity]. 
+    destruct (eq_dec x y); [contradiction | reflexivity].
   Qed.
 
 End Elts.
@@ -620,38 +602,38 @@ Section ListOps.
 
   Fixpoint rev (l:list A) : list A :=
     match l with
-      | nil => nil
-      | x :: l' => rev l' ++ x :: nil
+      | [] => []
+      | x :: l' => rev l' ++ [x]
     end.
 
-  Lemma distr_rev : forall x y:list A, rev (x ++ y) = rev y ++ rev x.
+  Lemma rev_app_distr : forall x y:list A, rev (x ++ y) = rev y ++ rev x.
   Proof.
     induction x as [| a l IHl].
     destruct y as [| a l].
-    simpl in |- *.
+    simpl.
     auto.
 
-    simpl in |- *.
-    apply app_nil_end; auto.
+    simpl.
+    rewrite app_nil_r; auto.
 
     intro y.
-    simpl in |- *.
+    simpl.
     rewrite (IHl y).
-    apply (app_ass (rev y) (rev l) (a :: nil)).
+    rewrite app_assoc; trivial.
   Qed.
 
-  Remark rev_unit : forall (l:list A) (a:A), rev (l ++ a :: nil) = a :: rev l.
+  Remark rev_unit : forall (l:list A) (a:A), rev (l ++ [a]) = a :: rev l.
   Proof.
     intros.
-    apply (distr_rev l (a :: nil)); simpl in |- *; auto.
+    apply (rev_app_distr l [a]); simpl; auto.
   Qed.
 
   Lemma rev_involutive : forall l:list A, rev (rev l) = l.
   Proof.
     induction l as [| a l IHl].
-    simpl in |- *; auto.
+    simpl; auto.
 
-    simpl in |- *.
+    simpl.
     rewrite (rev_unit (rev l) a).
     rewrite IHl; auto.
   Qed.
@@ -659,7 +641,7 @@ Section ListOps.
 
   (** Compatibility with other operations *)
 
-  Lemma In_rev : forall l x, In x l <-> In x (rev l).
+  Lemma in_rev : forall l x, In x l <-> In x (rev l).
   Proof.
     induction l.
     simpl; intuition.
@@ -681,7 +663,7 @@ Section ListOps.
     elim (length l); simpl; auto.
   Qed.
 
-  Lemma rev_nth : forall l d n,  n < length l ->  
+  Lemma rev_nth : forall l d n,  n < length l ->
     nth n (rev l) d = nth (length l - S n) l d.
   Proof.
     induction l.
@@ -704,309 +686,77 @@ Section ListOps.
   Qed.
 
 
-  (**  An alternative tail-recursive definition for reverse *) 
+  (**  An alternative tail-recursive definition for reverse *)
 
-  Fixpoint rev_append (l l': list A) {struct l} : list A := 
-    match l with 
-      | nil => l' 
+  Fixpoint rev_append (l l': list A) : list A :=
+    match l with
+      | [] => l'
       | a::l => rev_append l (a::l')
     end.
 
-  Definition rev' l : list A := rev_append l nil.
-
-  Notation rev_acc := rev_append (only parsing).
+  Definition rev' l : list A := rev_append l [].
 
-  Lemma rev_append_rev : forall l l', rev_acc l l' = rev l ++ l'.
+  Lemma rev_append_rev : forall l l', rev_append l l' = rev l ++ l'.
   Proof.
     induction l; simpl; auto; intros.
-    rewrite <- ass_app; firstorder.
+    rewrite <- app_assoc; firstorder.
   Qed.
 
-  Notation rev_acc_rev := rev_append_rev (only parsing).
-
-  Lemma rev_alt : forall l, rev l = rev_append l nil.
+  Lemma rev_alt : forall l, rev l = rev_append l [].
   Proof.
     intros; rewrite rev_append_rev.
-    apply app_nil_end.
+    rewrite app_nil_r; trivial.
   Qed.
 
 
 (*********************************************)
 (** Reverse Induction Principle on Lists  *)
 (*********************************************)
-  
+
   Section Reverse_Induction.
-    
-    Unset Implicit Arguments.
-    
+
     Lemma rev_list_ind :
       forall P:list A-> Prop,
-	P nil ->
+	P [] ->
 	(forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) ->
 	forall l:list A, P (rev l).
     Proof.
       induction l; auto.
     Qed.
-    Set Implicit Arguments.
-    
+
     Theorem rev_ind :
       forall P:list A -> Prop,
-	P nil ->
-	(forall (x:A) (l:list A), P l -> P (l ++ x :: nil)) -> forall l:list A, P l.
+	P [] ->
+	(forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l.
     Proof.
       intros.
       generalize (rev_involutive l).
       intros E; rewrite <- E.
       apply (rev_list_ind P).
       auto.
-      
-      simpl in |- *.
+
+      simpl.
       intros.
       apply (H0 a (rev l0)).
       auto.
     Qed.
-  
-  End Reverse_Induction.
-
-
-
-  (***********************************)
-  (** ** Lists modulo permutation    *)
-  (***********************************)
-  
-  Section Permutation.
-
-    Inductive Permutation : list A -> list A -> Prop :=
-      | perm_nil: Permutation nil nil
-      | perm_skip: forall (x:A) (l l':list A), Permutation l l' -> Permutation (cons x l) (cons x l')
-      | perm_swap: forall (x y:A) (l:list A), Permutation (cons y (cons x l)) (cons x (cons y l))
-      | perm_trans: forall (l l' l'':list A), Permutation l l' -> Permutation l' l'' -> Permutation l l''.
-
-    Hint Constructors Permutation.
-
-  (** Some facts about [Permutation] *)
-
-    Theorem Permutation_nil : forall (l : list A), Permutation nil l -> l = nil.
-    Proof.
-      intros l HF.
-      set (m:=@nil A) in HF; assert (m = nil); [reflexivity|idtac]; clearbody m.
-      induction HF; try elim (nil_cons (sym_eq H)); auto.
-    Qed.
-
-    Theorem Permutation_nil_cons : forall (l : list A) (x : A), ~ Permutation nil (x::l).
-    Proof.
-      unfold not; intros l x HF.
-      elim (@nil_cons A x l). apply sym_eq. exact (Permutation_nil HF).
-    Qed.
-
-  (** Permutation over lists is a equivalence relation *)
-
-    Theorem Permutation_refl : forall l : list A, Permutation l l.
-    Proof.
-      induction l; constructor. exact IHl. 
-    Qed.
-
-    Theorem Permutation_sym : forall l l' : list A, Permutation l l' -> Permutation l' l.
-    Proof.
-      intros l l' Hperm; induction Hperm; auto.
-      apply perm_trans with (l':=l'); assumption.
-    Qed.
-
-    Theorem Permutation_trans : forall l l' l'' : list A, Permutation l l' -> Permutation l' l'' -> Permutation l l''.
-    Proof.
-      exact perm_trans.
-    Qed.
-
-    Hint Resolve Permutation_refl Permutation_sym Permutation_trans.
-
-  (** Compatibility with others operations on lists *)
-
-    Theorem Permutation_in : forall (l l' : list A) (x : A), Permutation l l' -> In x l -> In x l'.
-    Proof.
-      intros l l' x Hperm; induction Hperm; simpl; tauto. 
-    Qed.
-
-    Lemma Permutation_app_tail : forall (l l' tl : list A), Permutation l l' -> Permutation (l++tl) (l'++tl).
-    Proof.
-      intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto.
-      eapply Permutation_trans with (l':=l'++tl); trivial.
-    Qed.
-
-    Lemma Permutation_app_head : forall (l tl tl' : list A), Permutation tl tl' -> Permutation (l++tl) (l++tl').
-    Proof.
-      intros l tl tl' Hperm; induction l; [trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
-    Qed.
-
-    Theorem Permutation_app : forall (l m l' m' : list A), Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').
-    Proof.
-      intros l m l' m' Hpermll' Hpermmm'; induction Hpermll' as [|x l l'|x y l|l l' l'']; repeat rewrite <- app_comm_cons; auto.
-      apply Permutation_trans with (l' := (x :: y :: l ++ m));
-	[idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial.
-      apply Permutation_trans with (l' := (l' ++ m')); try assumption.
-      apply Permutation_app_tail; assumption.
-    Qed.
-
-    Theorem Permutation_app_swap : forall (l l' : list A), Permutation (l++l') (l'++l).
-    Proof.
-      induction l as [|x l]. 
-      simpl; intro l'; rewrite <- app_nil_end; trivial.
-      induction l' as [|y l'].
-      simpl; rewrite <- app_nil_end; trivial.
-      simpl; apply Permutation_trans with (l' := x :: y :: l' ++ l).
-      constructor; rewrite app_comm_cons; apply IHl.
-      apply Permutation_trans with (l' := y :: x :: l' ++ l); constructor.
-      apply Permutation_trans with (l' := x :: l ++ l'); auto.
-    Qed.
-  
-    Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
-      Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
-    Proof.
-    intros l l1; revert l.
-    induction l1.
-    simpl.
-    intros; apply perm_skip; auto.
-    simpl; intros.
-    apply perm_trans with (a0::a::l1++l2).
-    apply perm_skip; auto.
-    apply perm_trans with (a::a0::l1++l2).
-    apply perm_swap; auto.
-    apply perm_skip; auto.
-    Qed.
-    Hint Resolve Permutation_cons_app.
-
-    Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'.
-    Proof.
-      intros l l' Hperm; induction Hperm; simpl; auto.
-      apply trans_eq with (y:= (length l')); trivial.
-    Qed.
-
-    Theorem Permutation_rev : forall (l : list A), Permutation l (rev l). 
-    Proof.
-      induction l as [| x l]; simpl; trivial.
-      apply Permutation_trans with (l' := (x::nil)++rev l).
-      simpl; auto.
-      apply Permutation_app_swap.
-    Qed.
-
-    Theorem Permutation_ind_bis : 
-     forall P : list A -> list A -> Prop,
-       P (@nil A) (@nil A) ->
-       (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
-       (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
-       (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
-       forall l l', Permutation l l' -> P l l'.
-    Proof.
-    intros P Hnil Hskip Hswap Htrans.
-    induction 1; auto.
-    apply Htrans with (x::y::l); auto.
-    apply Hswap; auto.
-    induction l; auto.
-    apply Hskip; auto.
-    apply Hskip; auto.
-    induction l; auto.
-    eauto.
-    Qed.
-
-    Ltac break_list l x l' H := 
-     destruct l as [|x l']; simpl in *; 
-     injection H; intros; subst; clear H.
-
-    Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
-      Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
-    Proof.
-    set (P:=fun l l' =>  
-             forall a l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 -> Permutation (l1++l2) (l3++l4)).
-    cut (forall l l', Permutation l l' -> P l l').
-    intros; apply (H _ _ H0 a); auto.
-    intros; apply (Permutation_ind_bis P); unfold P; clear P; try clear H l l'; simpl; auto.
-    (* nil *)
-    intros; destruct l1; simpl in *; discriminate.
-    (* skip *)
-    intros x l l' H IH; intros.
-    break_list l1 b l1' H0; break_list l3 c l3' H1.
-    auto.
-    apply perm_trans with (l3'++c::l4); auto.
-    apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app.
-    apply perm_skip.
-    apply (IH a l1' l2 l3' l4); auto.
-    (* contradict *)
-    intros x y l l' Hp IH; intros.
-    break_list l1 b l1' H; break_list l3 c l3' H0.
-    auto.
-    break_list l3' b l3'' H.
-    auto.
-    apply perm_trans with (c::l3''++b::l4); auto.
-    break_list l1' c l1'' H1. 
-    auto.
-    apply perm_trans with (b::l1''++c::l2); auto.
-    break_list l3' d l3'' H; break_list l1' e l1'' H1. 
-    auto.
-    apply perm_trans with (e::a::l1''++l2); auto.
-    apply perm_trans with (e::l1''++a::l2); auto.
-    apply perm_trans with (d::a::l3''++l4); auto.
-    apply perm_trans with (d::l3''++a::l4); auto.
-    apply perm_trans with (e::d::l1''++l2); auto.
-    apply perm_skip; apply perm_skip.
-    apply (IH a l1'' l2 l3'' l4); auto.
-    (*trans*)
-    intros.
-    destruct (In_split a l') as (l'1,(l'2,H6)).
-    apply (Permutation_in a H).
-    subst l.
-    apply in_or_app; right; red; auto.
-    apply perm_trans with (l'1++l'2).
-    apply (H0 _ _ _ _ _ H3 H6).
-    apply (H2 _ _ _ _ _ H6 H4).
-    Qed.
-
-    Theorem Permutation_cons_inv : 
-       forall l l' a, Permutation (a::l) (a::l') -> Permutation l l'.
-    Proof.
-    intros; exact (Permutation_app_inv (@nil _) l (@nil _) l' a H). 
-    Qed.
-
-    Theorem Permutation_cons_app_inv :
-       forall l l1 l2 a, Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
-    Proof.
-    intros; exact (Permutation_app_inv (@nil _) l l1 l2 a H). 
-    Qed.
-    
-    Theorem Permutation_app_inv_l : 
-        forall l l1 l2, Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
-    Proof.    
-    induction l; simpl; auto.
-    intros.
-    apply IHl.
-    apply Permutation_cons_inv with a; auto.
-    Qed.
-
-    Theorem Permutation_app_inv_r : 
-       forall l l1 l2, Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.
-    Proof.
-    induction l.
-    intros l1 l2; do 2 rewrite <- app_nil_end; auto.
-    intros.
-    apply IHl.
-    apply Permutation_app_inv with a; auto.
-    Qed.
-
-  End Permutation.
 
+  End Reverse_Induction.
 
   (***********************************)
   (** ** Decidable equality on lists *)
   (***********************************)
 
-  Hypotheses eqA_dec : forall (x y : A), {x = y}+{x <> y}.
+  Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}.
 
   Lemma list_eq_dec :
     forall l l':list A, {l = l'} + {l <> l'}.
   Proof.
     induction l as [| x l IHl]; destruct l' as [| y l'].
     left; trivial.
-    right; apply nil_cons. 
+    right; apply nil_cons.
     right; unfold not; intro HF; apply (nil_cons (sym_eq HF)).
-    destruct (eqA_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql']; 
+    destruct (eq_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql'];
       try (right; unfold not; intro HF; injection HF; intros; contradiction).
     rewrite xeqy; rewrite leql'; left; trivial.
   Qed.
@@ -1026,21 +776,19 @@ End ListOps.
 Section Map.
   Variables A B : Type.
   Variable f : A -> B.
-  
+
   Fixpoint map (l:list A) : list B :=
     match l with
       | nil => nil
       | cons a t => cons (f a) (map t)
     end.
-  
+
   Lemma in_map :
     forall (l:list A) (x:A), In x l -> In (f x) (map l).
-  Proof. 
-    induction l as [| a l IHl]; simpl in |- *;
-      [ auto
-	| destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ].
+  Proof.
+    induction l; firstorder (subst; auto).
   Qed.
-  
+
   Lemma in_map_iff : forall l y, In y (map l) <-> exists x, f x = y /\ In x l.
   Proof.
     induction l; firstorder (subst; auto).
@@ -1051,45 +799,48 @@ Section Map.
     induction l; simpl; auto.
   Qed.
 
-  Lemma map_nth : forall l d n, 
+  Lemma map_nth : forall l d n,
     nth n (map l) (f d) = f (nth n l d).
   Proof.
     induction l; simpl map; destruct n; firstorder.
   Qed.
-  
-  Lemma map_app : forall l l',  
+
+  Lemma map_nth_error : forall n l d,
+    nth_error l n = Some d -> nth_error (map l) n = Some (f d).
+  Proof.
+    induction n; intros [ | ] ? Heq; simpl in *; inversion Heq; auto.
+  Qed.
+
+  Lemma map_app : forall l l',
     map (l++l') = (map l)++(map l').
-  Proof. 
+  Proof.
     induction l; simpl; auto.
     intros; rewrite IHl; auto.
   Qed.
-  
+
   Lemma map_rev : forall l, map (rev l) = rev (map l).
-  Proof. 
+  Proof.
     induction l; simpl; auto.
     rewrite map_app.
     rewrite IHl; auto.
   Qed.
 
-  Hint Constructors Permutation.
-
-  Lemma Permutation_map : 
-    forall l l', Permutation l l' -> Permutation (map l) (map l').
-  Proof. 
-  induction 1; simpl; auto; eauto.
+  Lemma map_eq_nil : forall l, map l = [] -> l = [].
+  Proof.
+    destruct l; simpl; reflexivity || discriminate.
   Qed.
 
   (** [flat_map] *)
 
   Definition flat_map (f:A -> list B) :=
-    fix flat_map (l:list A) {struct l} : list B :=
+    fix flat_map (l:list A) : list B :=
     match l with
       | nil => nil
       | cons x t => (f x)++(flat_map t)
     end.
-  
+
   Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),
-    In y (flat_map f l) <-> exists x, In x l /\ In y (f x). 
+    In y (flat_map f l) <-> exists x, In x l /\ In y (f x).
   Proof.
     induction l; simpl; split; intros.
     contradiction.
@@ -1105,16 +856,22 @@ Section Map.
     exists x; auto.
   Qed.
 
-End Map. 
+End Map.
+
+Lemma map_id : forall (A :Type) (l : list A),
+  map (fun x => x) l = l.
+Proof.
+  induction l; simpl; auto; rewrite IHl; auto.
+Qed.
 
-Lemma map_map : forall (A B C:Type)(f:A->B)(g:B->C) l, 
+Lemma map_map : forall (A B C:Type)(f:A->B)(g:B->C) l,
   map g (map f l) = map (fun x => g (f x)) l.
 Proof.
   induction l; simpl; auto.
   rewrite IHl; auto.
 Qed.
 
-Lemma map_ext : 
+Lemma map_ext :
   forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l.
 Proof.
   induction l; simpl; auto.
@@ -1129,17 +886,17 @@ Qed.
 Section Fold_Left_Recursor.
   Variables A B : Type.
   Variable f : A -> B -> A.
-  
-  Fixpoint fold_left (l:list B) (a0:A) {struct l} : A :=
+
+  Fixpoint fold_left (l:list B) (a0:A) : A :=
     match l with
       | nil => a0
       | cons b t => fold_left t (f a0 b)
     end.
-  
-  Lemma fold_left_app : forall (l l':list B)(i:A), 
+
+  Lemma fold_left_app : forall (l l':list B)(i:A),
     fold_left (l++l') i = fold_left l' (fold_left l i).
   Proof.
-    induction l. 
+    induction l.
     simpl; auto.
     intros.
     simpl.
@@ -1148,7 +905,7 @@ Section Fold_Left_Recursor.
 
 End Fold_Left_Recursor.
 
-Lemma fold_left_length : 
+Lemma fold_left_length :
   forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l.
 Proof.
   intro A.
@@ -1168,7 +925,7 @@ Section Fold_Right_Recursor.
   Variables A B : Type.
   Variable f : B -> A -> A.
   Variable a0 : A.
-  
+
   Fixpoint fold_right (l:list B) : A :=
     match l with
       | nil => a0
@@ -1177,7 +934,7 @@ Section Fold_Right_Recursor.
 
 End Fold_Right_Recursor.
 
-  Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i, 
+  Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i,
     fold_right f i (l++l') = fold_right f (fold_right f i l') l.
   Proof.
     induction l.
@@ -1186,7 +943,7 @@ End Fold_Right_Recursor.
     f_equal; auto.
   Qed.
 
-  Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i, 
+  Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i,
     fold_right f i (rev l) = fold_left (fun x y => f y x) l i.
   Proof.
     induction l.
@@ -1204,10 +961,10 @@ End Fold_Right_Recursor.
   Proof.
     destruct l as [| a l].
     reflexivity.
-    simpl in |- *.
+    simpl.
     rewrite <- H0.
     generalize a0 a.
-    induction l as [| a3 l IHl]; simpl in |- *.
+    induction l as [| a3 l IHl]; simpl.
     trivial.
     intros.
     rewrite H.
@@ -1223,7 +980,7 @@ End Fold_Right_Recursor.
   (** [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
       indexed by elts of [x], sorted in lexicographic order. *)
 
-  Fixpoint list_power (A B:Type)(l:list A) (l':list B) {struct l} :
+  Fixpoint list_power (A B:Type)(l:list A) (l':list B) :
     list (list (A * B)) :=
     match l with
       | nil => cons nil nil
@@ -1237,20 +994,20 @@ End Fold_Right_Recursor.
   (** ** Boolean operations over lists *)
   (*************************************)
 
-  Section Bool. 
+  Section Bool.
     Variable A : Type.
     Variable f : A -> bool.
 
-  (** find whether a boolean function can be satisfied by an 
+  (** find whether a boolean function can be satisfied by an
        elements of the list. *)
 
-    Fixpoint existsb (l:list A) {struct l}: bool := 
-      match l with 
+    Fixpoint existsb (l:list A) : bool :=
+      match l with
 	| nil => false
 	| a::l => f a || existsb l
       end.
 
-    Lemma existsb_exists : 
+    Lemma existsb_exists :
       forall l, existsb l = true <-> exists x, In x l /\ f x = true.
     Proof.
       induction l; simpl; intuition.
@@ -1269,20 +1026,28 @@ End Fold_Right_Recursor.
       inversion 1.
       simpl; intros.
       destruct (orb_false_elim _ _ H0); clear H0; auto.
-      destruct n ; auto. 
+      destruct n ; auto.
       rewrite IHl; auto with arith.
     Qed.
 
-  (** find whether a boolean function is satisfied by 
+    Lemma existsb_app : forall l1 l2,
+      existsb (l1++l2) = existsb l1 || existsb l2.
+    Proof.
+      induction l1; intros l2; simpl.
+        solve[auto].
+      case (f a); simpl; solve[auto].
+    Qed.
+
+  (** find whether a boolean function is satisfied by
     all the elements of a list. *)
 
-    Fixpoint forallb (l:list A) {struct l} : bool := 
-      match l with 
+    Fixpoint forallb (l:list A) : bool :=
+      match l with
 	| nil => true
 	| a::l => f a && forallb l
       end.
 
-    Lemma forallb_forall : 
+    Lemma forallb_forall :
       forall l, forallb l = true <-> (forall x, In x l -> f x = true).
     Proof.
       induction l; simpl; intuition.
@@ -1291,13 +1056,20 @@ End Fold_Right_Recursor.
       destruct (andb_prop _ _ H1); auto.
       assert (forallb l = true).
       apply H0; intuition.
-      rewrite H1; auto. 
+      rewrite H1; auto.
     Qed.
 
+    Lemma forallb_app :
+      forall l1 l2, forallb (l1++l2) = forallb l1 && forallb l2.
+    Proof.
+      induction l1; simpl.
+        solve[auto].
+      case (f a); simpl; solve[auto].
+    Qed.
   (** [filter] *)
 
-    Fixpoint filter (l:list A) : list A := 
-      match l with 
+    Fixpoint filter (l:list A) : list A :=
+      match l with
 	| nil => nil
 	| x :: l => if f x then x::(filter l) else filter l
       end.
@@ -1320,10 +1092,10 @@ End Fold_Right_Recursor.
 
   (** [partition] *)
 
-    Fixpoint partition (l:list A) {struct l} : list A * list A := 
+    Fixpoint partition (l:list A) : list A * list A :=
       match l with
 	| nil => (nil, nil)
-	| x :: tl => let (g,d) := partition tl in 
+	| x :: tl => let (g,d) := partition tl in
 	  if f x then (x::g,d) else (g,x::d)
       end.
 
@@ -1338,17 +1110,17 @@ End Fold_Right_Recursor.
 
   Section ListPairs.
     Variables A B : Type.
-    
+
   (** [split] derives two lists from a list of pairs *)
 
-    Fixpoint split  (l:list (A*B)) { struct l }: list A * list B :=
+    Fixpoint split (l:list (A*B)) : list A * list B :=
       match l with
 	| nil => (nil, nil)
 	| (x,y) :: tl => let (g,d) := split tl in (x::g, y::d)
       end.
 
-    Lemma in_split_l : forall (l:list (A*B))(p:A*B), 
-      In p l -> In (fst p) (fst (split l)). 
+    Lemma in_split_l : forall (l:list (A*B))(p:A*B),
+      In p l -> In (fst p) (fst (split l)).
     Proof.
       induction l; simpl; intros; auto.
       destruct p; destruct a; destruct (split l); simpl in *.
@@ -1357,8 +1129,8 @@ End Fold_Right_Recursor.
       right; apply (IHl (a0,b) H).
     Qed.
 
-    Lemma in_split_r : forall (l:list (A*B))(p:A*B), 
-      In p l -> In (snd p) (snd (split l)). 
+    Lemma in_split_r : forall (l:list (A*B))(p:A*B),
+      In p l -> In (snd p) (snd (split l)).
     Proof.
       induction l; simpl; intros; auto.
       destruct p; destruct a; destruct (split l); simpl in *.
@@ -1367,7 +1139,7 @@ End Fold_Right_Recursor.
       right; apply (IHl (a0,b) H).
     Qed.
 
-    Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B), 
+    Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B),
       nth n l d = (nth n (fst (split l)) (fst d), nth n (snd (split l)) (snd d)).
     Proof.
       induction l.
@@ -1379,40 +1151,40 @@ End Fold_Right_Recursor.
     Qed.
 
     Lemma split_length_l : forall (l:list (A*B)),
-      length (fst (split l)) = length l. 
+      length (fst (split l)) = length l.
     Proof.
       induction l; simpl; auto.
       destruct a; destruct (split l); simpl; auto.
     Qed.
 
     Lemma split_length_r : forall (l:list (A*B)),
-      length (snd (split l)) = length l. 
+      length (snd (split l)) = length l.
     Proof.
       induction l; simpl; auto.
       destruct a; destruct (split l); simpl; auto.
     Qed.
 
-  (** [combine] is the opposite of [split]. 
-      Lists given to [combine] are meant to be of same length. 
+  (** [combine] is the opposite of [split].
+      Lists given to [combine] are meant to be of same length.
       If not, [combine] stops on the shorter list *)
 
-    Fixpoint combine (l : list A) (l' : list B){struct l} : list (A*B) :=
+    Fixpoint combine (l : list A) (l' : list B) : list (A*B) :=
       match l,l' with
 	| x::tl, y::tl' => (x,y)::(combine tl tl')
 	| _, _ => nil
       end.
 
-    Lemma split_combine : forall (l: list (A*B)), 
+    Lemma split_combine : forall (l: list (A*B)),
       let (l1,l2) := split l in combine l1 l2 = l.
     Proof.
       induction l.
       simpl; auto.
-      destruct a; simpl. 
+      destruct a; simpl.
       destruct (split l); simpl in *.
       f_equal; auto.
     Qed.
 
-    Lemma combine_split : forall (l:list A)(l':list B), length l = length l' -> 
+    Lemma combine_split : forall (l:list A)(l':list B), length l = length l' ->
       split (combine l l') = (l,l').
     Proof.
       induction l; destruct l'; simpl; intros; auto; try discriminate.
@@ -1420,19 +1192,19 @@ End Fold_Right_Recursor.
       rewrite IHl; auto.
     Qed.
 
-    Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B), 
+    Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B),
       In (x,y) (combine l l') -> In x l.
     Proof.
       induction l.
       simpl; auto.
       destruct l'; simpl; auto; intros.
-      contradiction. 
+      contradiction.
       destruct H.
       injection H; auto.
       right; apply IHl with l' y; auto.
     Qed.
 
-    Lemma in_combine_r : forall (l:list A)(l':list B)(x:A)(y:B), 
+    Lemma in_combine_r : forall (l:list A)(l':list B)(x:A)(y:B),
       In (x,y) (combine l l') -> In y l'.
     Proof.
       induction l.
@@ -1443,7 +1215,7 @@ End Fold_Right_Recursor.
       right; apply IHl with x; auto.
     Qed.
 
-    Lemma combine_length : forall (l:list A)(l':list B), 
+    Lemma combine_length : forall (l:list A)(l':list B),
       length (combine l l') = min (length l) (length l').
     Proof.
       induction l.
@@ -1451,8 +1223,8 @@ End Fold_Right_Recursor.
       destruct l'; simpl; auto.
     Qed.
 
-    Lemma combine_nth : forall (l:list A)(l':list B)(n:nat)(x:A)(y:B), 
-      length l = length l' -> 
+    Lemma combine_nth : forall (l:list A)(l':list B)(n:nat)(x:A)(y:B),
+      length l = length l' ->
       nth n (combine l l') (x,y) = (nth n l x, nth n l' y).
     Proof.
       induction l; destruct l'; intros; try discriminate.
@@ -1461,10 +1233,10 @@ End Fold_Right_Recursor.
     Qed.
 
   (** [list_prod] has the same signature as [combine], but unlike
-     [combine], it adds every possible pairs, not only those at the 
+     [combine], it adds every possible pairs, not only those at the
      same position. *)
 
-    Fixpoint list_prod (l:list A) (l':list B) {struct l} :
+    Fixpoint list_prod (l:list A) (l':list B) :
       list (A * B) :=
       match l with
 	| nil => nil
@@ -1474,25 +1246,25 @@ End Fold_Right_Recursor.
     Lemma in_prod_aux :
       forall (x:A) (y:B) (l:list B),
 	In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).
-    Proof. 
+    Proof.
       induction l;
-	[ simpl in |- *; auto
-	  | simpl in |- *; destruct 1 as [H1| ];
+	[ simpl; auto
+	  | simpl; destruct 1 as [H1| ];
 	    [ left; rewrite H1; trivial | right; auto ] ].
     Qed.
 
     Lemma in_prod :
       forall (l:list A) (l':list B) (x:A) (y:B),
 	In x l -> In y l' -> In (x, y) (list_prod l l').
-    Proof. 
+    Proof.
       induction l;
-	[ simpl in |- *; tauto
-	  | simpl in |- *; intros; apply in_or_app; destruct H;
+	[ simpl; tauto
+	  | simpl; intros; apply in_or_app; destruct H;
 	    [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ].
     Qed.
 
-    Lemma in_prod_iff : 
-      forall (l:list A)(l':list B)(x:A)(y:B), 
+    Lemma in_prod_iff :
+      forall (l:list A)(l':list B)(x:A)(y:B),
 	In (x,y) (list_prod l l') <-> In x l /\ In y l'.
     Proof.
       split; [ | intros; apply in_prod; intuition ].
@@ -1503,9 +1275,9 @@ End Fold_Right_Recursor.
       destruct (H1 H0) as (z,(H2,H3)); clear H0 H1.
       injection H2; clear H2; intros; subst; intuition.
       intuition.
-    Qed. 
+    Qed.
 
-    Lemma prod_length : forall (l:list A)(l':list B), 
+    Lemma prod_length : forall (l:list A)(l':list B),
       length (list_prod l l') = (length l) * (length l').
     Proof.
       induction l; simpl; auto.
@@ -1520,9 +1292,9 @@ End Fold_Right_Recursor.
 
 
 
-(***************************************)
-(** * Miscelenous operations on lists  *)
-(***************************************)
+(*****************************************)
+(** * Miscellaneous operations on lists  *)
+(*****************************************)
 
 
 
@@ -1539,34 +1311,34 @@ Section length_order.
   Variables l m n : list A.
 
   Lemma lel_refl : lel l l.
-  Proof. 
-    unfold lel in |- *; auto with arith.
+  Proof.
+    unfold lel; auto with arith.
   Qed.
 
   Lemma lel_trans : lel l m -> lel m n -> lel l n.
-  Proof. 
-    unfold lel in |- *; intros.
+  Proof.
+    unfold lel; intros.
     now_show (length l <= length n).
     apply le_trans with (length m); auto with arith.
   Qed.
 
   Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).
-  Proof. 
-    unfold lel in |- *; simpl in |- *; auto with arith.
+  Proof.
+    unfold lel; simpl; auto with arith.
   Qed.
 
   Lemma lel_cons : lel l m -> lel l (b :: m).
-  Proof. 
-    unfold lel in |- *; simpl in |- *; auto with arith.
+  Proof.
+    unfold lel; simpl; auto with arith.
   Qed.
 
   Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m.
-  Proof. 
-    unfold lel in |- *; simpl in |- *; auto with arith.
+  Proof.
+    unfold lel; simpl; auto with arith.
   Qed.
 
   Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'.
-  Proof. 
+  Proof.
     intro l'; elim l'; auto with arith.
     intros a' y H H0.
     now_show (nil = a' :: y).
@@ -1588,40 +1360,40 @@ Section SetIncl.
 
   Definition incl (l m:list A) := forall a:A, In a l -> In a m.
   Hint Unfold incl.
-  
+
   Lemma incl_refl : forall l:list A, incl l l.
-  Proof. 
+  Proof.
     auto.
   Qed.
   Hint Resolve incl_refl.
-  
+
   Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
-  Proof. 
+  Proof.
     auto with datatypes.
   Qed.
   Hint Immediate incl_tl.
 
   Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n.
-  Proof. 
+  Proof.
     auto.
   Qed.
-  
+
   Lemma incl_appl : forall l m n:list A, incl l n -> incl l (n ++ m).
-  Proof. 
+  Proof.
     auto with datatypes.
   Qed.
   Hint Immediate incl_appl.
-  
+
   Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
-  Proof. 
+  Proof.
     auto with datatypes.
   Qed.
   Hint Immediate incl_appr.
-  
+
   Lemma incl_cons :
     forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m.
-  Proof. 
-    unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
+  Proof.
+    unfold incl; simpl; intros a l m H H0 a0 H1.
     now_show (In a0 m).
     elim H1.
     now_show (a = a0 -> In a0 m).
@@ -1632,15 +1404,15 @@ Section SetIncl.
     auto.
   Qed.
   Hint Resolve incl_cons.
-  
+
   Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n.
-  Proof. 
-    unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
+  Proof.
+    unfold incl; simpl; intros l m n H H0 a H1.
     now_show (In a n).
     elim (in_app_or _ _ _ H1); auto.
   Qed.
   Hint Resolve incl_app.
-  
+
 End SetIncl.
 
 Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
@@ -1655,24 +1427,24 @@ Section Cutting.
 
   Variable A : Type.
 
-  Fixpoint firstn (n:nat)(l:list A) {struct n} : list A := 
-    match n with 
-      | 0 => nil 
-      | S n => match l with  
-		 | nil => nil 
+  Fixpoint firstn (n:nat)(l:list A) : list A :=
+    match n with
+      | 0 => nil
+      | S n => match l with
+		 | nil => nil
 		 | a::l => a::(firstn n l)
 	       end
     end.
-  
-  Fixpoint skipn (n:nat)(l:list A) { struct n } : list A := 
-    match n with 
-      | 0 => l 
-      | S n => match l with 
-		 | nil => nil 
+
+  Fixpoint skipn (n:nat)(l:list A) : list A :=
+    match n with
+      | 0 => l
+      | S n => match l with
+		 | nil => nil
 		 | a::l => skipn n l
 	       end
     end.
-  
+
   Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l.
   Proof.
     induction n.
@@ -1686,7 +1458,7 @@ Section Cutting.
     induction n; destruct l; simpl; auto.
   Qed.
 
-   Lemma removelast_firstn : forall n l, n < length l -> 
+   Lemma removelast_firstn : forall n l, n < length l ->
      removelast (firstn (S n) l) = firstn n l.
    Proof.
      induction n; destruct l.
@@ -1699,13 +1471,13 @@ Section Cutting.
      change (firstn (S n) (a::l)) with (a::firstn n l).
      rewrite removelast_app.
      rewrite IHn; auto with arith.
-     
+
      clear IHn; destruct l; simpl in *; try discriminate.
      inversion_clear H.
      inversion_clear H0.
    Qed.
 
-   Lemma firstn_removelast : forall n l, n < length l -> 
+   Lemma firstn_removelast : forall n l, n < length l ->
      firstn n (removelast l) = firstn n l.
    Proof.
      induction n; destruct l.
@@ -1730,10 +1502,10 @@ End Cutting.
 Section ReDun.
 
   Variable A : Type.
-  
-  Inductive NoDup : list A -> Prop := 
-    | NoDup_nil : NoDup nil 
-    | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). 
+
+  Inductive NoDup : list A -> Prop :=
+    | NoDup_nil : NoDup nil
+    | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l).
 
   Lemma NoDup_remove_1 : forall l l' a, NoDup (l++a::l') -> NoDup (l++l').
   Proof.
@@ -1758,34 +1530,6 @@ Section ReDun.
   destruct (IHl _ _ H1); auto.
   Qed.
 
-  Lemma NoDup_Permutation : forall l l', 
-    NoDup l -> NoDup l' -> (forall x, In x l <-> In x l') -> Permutation l l'.
-  Proof.
-  induction l. 
-  destruct l'; simpl; intros.
-  apply perm_nil.
-  destruct (H1 a) as (_,H2); destruct H2; auto.
-  intros.
-  destruct (In_split a l') as (l'1,(l'2,H2)).
-  destruct (H1 a) as (H2,H3); simpl in *; auto.
-  subst l'.
-  apply Permutation_cons_app.
-  inversion_clear H.
-  apply IHl; auto.
-  apply NoDup_remove_1 with a; auto.
-  intro x; split; intros.
-  assert (In x (l'1++a::l'2)).
-   destruct (H1 x); simpl in *; auto.
-  apply in_or_app; destruct (in_app_or _ _ _ H4); auto.
-  destruct H5; auto.
-  subst x; destruct H2; auto.
-  assert (In x (l'1++a::l'2)).
-    apply in_or_app; destruct (in_app_or _ _ _ H); simpl; auto.
-  destruct (H1 x) as (_,H5); destruct H5; auto. 
-  subst x.
-  destruct (NoDup_remove_2 _ _ _ H0 H).
-  Qed.
-
 End ReDun.
 
 
@@ -1795,21 +1539,21 @@ End ReDun.
 
 Section NatSeq.
 
-  (** [seq] computes the sequence of [len] contiguous integers 
+  (** [seq] computes the sequence of [len] contiguous integers
       that starts at [start]. For instance, [seq 2 3] is [2::3::4::nil]. *)
-  
-  Fixpoint seq (start len:nat) {struct len} : list nat := 
-    match len with 
+
+  Fixpoint seq (start len:nat) : list nat :=
+    match len with
       | 0 => nil
       | S len => start :: seq (S start) len
-    end. 
-  
+    end.
+
   Lemma seq_length : forall len start, length (seq start len) = len.
   Proof.
     induction len; simpl; auto.
   Qed.
-  
-  Lemma seq_nth : forall len start n d, 
+
+  Lemma seq_nth : forall len start n d,
     n < len -> nth n (seq start len) d = start+n.
   Proof.
     induction len; intros.
@@ -1822,7 +1566,7 @@ Section NatSeq.
 
   Lemma seq_shift : forall len start,
     map S (seq start len) = seq (S start) len.
-  Proof. 
+  Proof.
     induction len; simpl; auto.
     intros.
     rewrite IHlen.
@@ -1832,11 +1576,172 @@ Section NatSeq.
 End NatSeq.
 
 
+(** * Existential and universal predicates over lists *)
+
+Inductive Exists {A} (P:A->Prop) : list A -> Prop :=
+ | Exists_cons_hd : forall x l, P x -> Exists P (x::l)
+ | Exists_cons_tl : forall x l, Exists P l -> Exists P (x::l).
+Hint Constructors Exists.
+
+Lemma Exists_exists : forall A P (l:list A),
+ Exists P l <-> (exists x, In x l /\ P x).
+Proof.
+split.
+induction 1; firstorder.
+induction l; firstorder; subst; auto.
+Qed.
+
+Lemma Exists_nil : forall A (P:A->Prop), Exists P nil <-> False.
+Proof. split; inversion 1. Qed.
+
+Lemma Exists_cons : forall A (P:A->Prop) x l,
+ Exists P (x::l) <-> P x \/ Exists P l.
+Proof. split; inversion 1; auto. Qed.
+
+
+Inductive Forall {A} (P:A->Prop) : list A -> Prop :=
+ | Forall_nil : Forall P nil
+ | Forall_cons : forall x l, P x -> Forall P l -> Forall P (x::l).
+Hint Constructors Forall.
 
-  (** * Exporting hints and tactics *)
+Lemma Forall_forall : forall A P (l:list A),
+ Forall P l <-> (forall x, In x l -> P x).
+Proof.
+split.
+induction 1; firstorder; subst; auto.
+induction l; firstorder.
+Qed.
+
+Lemma Forall_inv : forall A P (a:A) l, Forall P (a :: l) -> P a.
+Proof.
+intros; inversion H; trivial.
+Defined.
+
+Lemma Forall_rect : forall A (P:A->Prop) (Q : list A -> Type),
+     Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall P l -> Q l.
+Proof.
+intros A P Q H H'; induction l; intro; [|eapply H', Forall_inv]; eassumption.
+Defined.
+
+Lemma Forall_impl : forall A (P Q : A -> Prop), (forall a, P a -> Q a) ->
+  forall l, Forall P l -> Forall Q l.
+Proof.
+  intros A P Q Himp l H.
+  induction H; firstorder.
+Qed.
 
+(** [Forall2]: stating that elements of two lists are pairwise related. *)
 
-Hint Rewrite 
+Inductive Forall2 A B (R:A->B->Prop) : list A -> list B -> Prop :=
+ | Forall2_nil : Forall2 R [] []
+ | Forall2_cons : forall x y l l',
+    R x y -> Forall2 R l l' -> Forall2 R (x::l) (y::l').
+Hint Constructors Forall2.
+
+Theorem Forall2_refl : forall A B (R:A->B->Prop), Forall2 R [] [].
+Proof. exact Forall2_nil. Qed.
+
+Theorem Forall2_app_inv_l : forall A B (R:A->B->Prop) l1 l2 l',
+  Forall2 R (l1 ++ l2) l' ->
+  exists l1', exists l2', Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l' = l1' ++ l2'.
+Proof.
+  induction l1; intros.
+    exists [], l'; auto.
+    simpl in H; inversion H; subst; clear H.
+    apply IHl1 in H4 as (l1' & l2' & Hl1 & Hl2 & ->).
+    exists (y::l1'), l2'; simpl; auto.
+Qed.
+
+Theorem Forall2_app_inv_r : forall A B (R:A->B->Prop) l1' l2' l,
+  Forall2 R l (l1' ++ l2') ->
+  exists l1, exists l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2.
+Proof.
+  induction l1'; intros.
+    exists [], l; auto.
+    simpl in H; inversion H; subst; clear H.
+    apply IHl1' in H4 as (l1 & l2 & Hl1 & Hl2 & ->).
+    exists (x::l1), l2; simpl; auto.
+Qed.
+
+Theorem Forall2_app : forall A B (R:A->B->Prop) l1 l2 l1' l2',
+  Forall2 R l1 l1' -> Forall2 R l2 l2' -> Forall2 R (l1 ++ l2) (l1' ++ l2').
+Proof.
+  intros. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto.
+Qed.
+
+(** [ForallPairs] : specifies that a certain relation should
+    always hold when inspecting all possible pairs of elements of a list. *)
+
+Definition ForallPairs A (R : A -> A -> Prop) l :=
+ forall a b, In a l -> In b l -> R a b.
+
+(** [ForallOrdPairs] : we still check a relation over all pairs
+     of elements of a list, but now the order of elements matters. *)
+
+Inductive ForallOrdPairs A (R : A -> A -> Prop) : list A -> Prop :=
+  | FOP_nil : ForallOrdPairs R nil
+  | FOP_cons : forall a l,
+     Forall (R a) l -> ForallOrdPairs R l -> ForallOrdPairs R (a::l).
+Hint Constructors ForallOrdPairs.
+
+Lemma ForallOrdPairs_In : forall A (R:A->A->Prop) l,
+ ForallOrdPairs R l ->
+ forall x y, In x l -> In y l -> x=y \/ R x y \/ R y x.
+Proof.
+ induction 1.
+ inversion 1.
+ simpl; destruct 1; destruct 1; repeat subst; auto.
+ right; left. apply -> Forall_forall; eauto.
+ right; right. apply -> Forall_forall; eauto.
+Qed.
+
+
+(** [ForallPairs] implies [ForallOrdPairs]. The reverse implication is true
+    only when [R] is symmetric and reflexive. *)
+
+Lemma ForallPairs_ForallOrdPairs : forall A (R:A->A->Prop) l,
+ ForallPairs R l -> ForallOrdPairs R l.
+Proof.
+ induction l; auto. intros H.
+ constructor.
+ apply <- Forall_forall. intros; apply H; simpl; auto.
+ apply IHl. red; intros; apply H; simpl; auto.
+Qed.
+
+Lemma ForallOrdPairs_ForallPairs : forall A (R:A->A->Prop),
+ (forall x, R x x) ->
+ (forall x y, R x y -> R y x) ->
+ forall l, ForallOrdPairs R l -> ForallPairs R l.
+Proof.
+ intros A R Refl Sym l Hl x y Hx Hy.
+ destruct (ForallOrdPairs_In Hl _ _ Hx Hy); subst; intuition.
+Qed.
+
+(** * Inversion of predicates over lists based on head symbol *)
+
+Ltac is_list_constr c :=
+ match c with
+  | nil => idtac
+  | (_::_) => idtac
+  | _ => fail
+ end.
+
+Ltac invlist f :=
+ match goal with
+  | H:f ?l |- _ => is_list_constr l; inversion_clear H; invlist f
+  | H:f _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f
+  | H:f _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f
+  | H:f _ _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f
+  | H:f _ _ _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f
+  | _ => idtac
+ end.
+
+
+
+(** * Exporting hints and tactics *)
+
+
+Hint Rewrite
   rev_involutive (* rev (rev l) = l *)
   rev_unit (* rev (l ++ a :: nil) = a :: rev l *)
   map_nth (* nth n (map f l) (f d) = f (nth n l d) *)
@@ -1844,11 +1749,36 @@ Hint Rewrite
   seq_length (* length (seq start len) = len *)
   app_length (* length (l ++ l') = length l + length l' *)
   rev_length (* length (rev l) = length l *)
-  : list.
-
-Hint Rewrite <- 
-  app_nil_end (* l = l ++ nil *)
+  app_nil_r (* l ++ nil = l *)
   : list.
 
 Ltac simpl_list := autorewrite with list.
 Ltac ssimpl_list := autorewrite with list using simpl.
+
+(* begin hide *)
+(* Compatibility notations after the migration of [list] to [Datatypes] *)
+Notation list := list (only parsing).
+Notation list_rect := list_rect (only parsing).
+Notation list_rec := list_rec (only parsing).
+Notation list_ind := list_ind (only parsing).
+Notation nil := nil (only parsing).
+Notation cons := cons (only parsing).
+Notation length := length (only parsing).
+Notation app := app (only parsing).
+(* Compatibility Names *)
+Notation tail := tl (only parsing).
+Notation head := hd_error (only parsing).
+Notation head_nil := hd_error_nil (only parsing).
+Notation head_cons := hd_error_cons (only parsing).
+Notation ass_app := app_assoc (only parsing).
+Notation app_ass := app_assoc_reverse (only parsing).
+Notation In_split := in_split (only parsing).
+Notation In_rev := in_rev (only parsing).
+Notation In_dec := in_dec (only parsing).
+Notation distr_rev := rev_app_distr (only parsing).
+Notation rev_acc := rev_append (only parsing).
+Notation rev_acc_rev := rev_append_rev (only parsing).
+Notation AllS := Forall (only parsing). (* was formerly in TheoryList *)
+
+Hint Resolve app_nil_end : datatypes v62.
+(* end hide *)
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 021a64c1..20c9e7e8 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ListSet.v 10616 2008-03-04 17:33:35Z letouzey $ i*)
+(*i $Id$ i*)
 
 (** A Library for finite sets, implemented as lists *)
 
@@ -27,7 +27,7 @@ Section first_definitions.
 
   Definition empty_set : set := nil.
 
-  Fixpoint set_add (a:A) (x:set) {struct x} : set :=
+  Fixpoint set_add (a:A) (x:set) : set :=
     match x with
     | nil => a :: nil
     | a1 :: x1 =>
@@ -38,7 +38,7 @@ Section first_definitions.
     end.
 
 
-  Fixpoint set_mem (a:A) (x:set) {struct x} : bool :=
+  Fixpoint set_mem (a:A) (x:set) : bool :=
     match x with
     | nil => false
     | a1 :: x1 =>
@@ -47,9 +47,9 @@ Section first_definitions.
         | right _ => set_mem a x1
         end
     end.
- 
+
   (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
-  Fixpoint set_remove (a:A) (x:set) {struct x} : set :=
+  Fixpoint set_remove (a:A) (x:set) : set :=
     match x with
     | nil => empty_set
     | a1 :: x1 =>
@@ -67,20 +67,20 @@ Section first_definitions.
           if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y
     end.
 
-  Fixpoint set_union (x y:set) {struct y} : set :=
+  Fixpoint set_union (x y:set) : set :=
     match y with
     | nil => x
     | a1 :: y1 => set_add a1 (set_union x y1)
     end.
-        
+
   (** returns the set of all els of [x] that does not belong to [y] *)
-  Fixpoint set_diff (x y:set) {struct x} : set :=
+  Fixpoint set_diff (x y:set) : set :=
     match x with
     | nil => nil
     | a1 :: x1 =>
         if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y)
     end.
-   
+
 
   Definition set_In : A -> set -> Prop := In (A:=A).
 
@@ -123,7 +123,7 @@ Section first_definitions.
     case H3; auto.
   Qed.
 
- 
+
   Lemma set_mem_correct1 :
    forall (a:A) (x:set), set_mem a x = true -> set_In a x.
   Proof.
@@ -191,11 +191,11 @@ Section first_definitions.
 
   Lemma set_add_intro :
    forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).
-  
+
   Proof.
     intros a b x [H1| H2]; auto with datatypes.
   Qed.
- 
+
   Lemma set_add_elim :
    forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.
 
@@ -225,7 +225,7 @@ Section first_definitions.
     simple induction x; simpl in |- *.
     discriminate.
     intros; elim (Aeq_dec a a0); intros; discriminate.
-  Qed.   
+  Qed.
 
 
   Lemma set_union_intro1 :
@@ -289,7 +289,7 @@ Section first_definitions.
     elim (set_mem a y); simpl in |- *; intros.
     auto with datatypes.
     absurd (set_In a y); auto with datatypes.
-    elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].     
+    elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].
   Qed.
 
   Lemma set_inter_elim1 :
@@ -324,7 +324,7 @@ Section first_definitions.
      set_In a (set_inter x y) -> set_In a x /\ set_In a y.
   Proof.
     eauto with datatypes.
-  Qed. 
+  Qed.
 
   Lemma set_diff_intro :
    forall (a:A) (x y:set),
@@ -354,7 +354,7 @@ Section first_definitions.
    forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.
   intros a x y; elim x; simpl in |- *.
   intros; contradiction.
-  intros a0 l Hrec. 
+  intros a0 l Hrec.
   apply set_mem_ind2; auto.
   intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto.
   rewrite H; trivial.
@@ -373,24 +373,23 @@ End first_definitions.
 
 Section other_definitions.
 
-  Variables A B : Type.
-
-  Definition set_prod : set A -> set B -> set (A * B) :=
-    list_prod (A:=A) (B:=B).
+  Definition set_prod : forall {A B:Type}, set A -> set B -> set (A * B) :=
+    list_prod.
 
   (** [B^A], set of applications from [A] to [B] *)
-  Definition set_power : set A -> set B -> set (set (A * B)) :=
-    list_power (A:=A) (B:=B).
+  Definition set_power : forall {A B:Type}, set A -> set B -> set (set (A * B)) :=
+    list_power.
 
-  Definition set_map : (A -> B) -> set A -> set B := map (A:=A) (B:=B).
-
-  Definition set_fold_left : (B -> A -> B) -> set A -> B -> B :=
+  Definition set_fold_left {A B:Type} : (B -> A -> B) -> set A -> B -> B :=
     fold_left (A:=B) (B:=A).
 
-  Definition set_fold_right (f:A -> B -> B) (x:set A) 
+  Definition set_fold_right {A B:Type} (f:A -> B -> B) (x:set A)
     (b:B) : B := fold_right f b x.
 
- 
+  Definition set_map {A B:Type} (Aeq_dec : forall x y:B, {x = y} + {x <> y})
+    (f : A -> B) (x : set A) : set B :=
+    set_fold_right (fun a => set_add Aeq_dec (f a)) x (empty_set B).
+
 End other_definitions.
 
 Unset Implicit Arguments.
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 515ed138..0a21a9e2 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -6,40 +6,44 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ListTactics.v 9427 2006-12-11 18:46:35Z bgregoir $ i*)
+(*i $Id$ i*)
 
 Require Import BinPos.
 Require Import List.
 
 Ltac list_fold_right fcons fnil l :=
   match l with
-  | (cons ?x ?tl) => fcons x ltac:(list_fold_right fcons fnil tl)
+  | ?x :: ?tl => fcons x ltac:(list_fold_right fcons fnil tl)
   | nil => fnil
   end.
 
+(* A variant of list_fold_right, to prevent the match of list_fold_right
+   from catching errors raised by fcons. *)
 Ltac lazy_list_fold_right fcons fnil l :=
-  match l with
-  | (cons ?x ?tl) => 
-       let cont := lazy_list_fold_right fcons fnil in
-       fcons x cont tl
-  | nil => fnil 
-  end.
+  let f :=
+    match l with
+    | ?x :: ?tl =>
+         fun _ =>
+         fcons x ltac:(fun _ => lazy_list_fold_right fcons fnil tl)
+    | nil => fun _ => fnil()
+    end in
+  f().
 
 Ltac list_fold_left fcons fnil l :=
   match l with
-  | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl
+  | ?x :: ?tl => list_fold_left fcons ltac:(fcons x fnil) tl
   | nil => fnil
   end.
 
 Ltac list_iter f l :=
   match l with
-  | (cons ?x ?tl) => f x; list_iter f tl
+  | ?x :: ?tl => f x; list_iter f tl
   | nil => idtac
   end.
 
 Ltac list_iter_gen seq f l :=
   match l with
-  | (cons ?x ?tl) =>
+  | ?x :: ?tl =>
       let t1 _ := f x in
       let t2 _ := list_iter_gen seq f tl in
       seq t1 t2
@@ -48,30 +52,30 @@ Ltac list_iter_gen seq f l :=
 
 Ltac AddFvTail a l :=
  match l with
- | nil          => constr:(cons a l)
- | (cons a _)   => l
- | (cons ?x ?l) => let l' := AddFvTail a l in constr:(cons x l')
+ | nil      => constr:(a::nil)
+ | a :: _   => l
+ | ?x :: ?l => let l' := AddFvTail a l in constr:(x::l')
  end.
 
 Ltac Find_at a l :=
  let rec find n l :=
    match l with
-   | nil => fail 100 "anomaly: Find_at"
-   | (cons a _) => eval compute in n
-   | (cons _ ?l) => find (Psucc n) l
+   | nil     => fail 100 "anomaly: Find_at"
+   | a :: _  => eval compute in n
+   | _ :: ?l => find (Psucc n) l
    end
  in find 1%positive l.
 
 Ltac check_is_list t :=
   match t with
-  | cons _ ?l => check_is_list l
-  | nil => idtac
-  | _ => fail 100 "anomaly: failed to build a canonical list"
+  | _ :: ?l => check_is_list l
+  | nil     => idtac
+  | _       => fail 100 "anomaly: failed to build a canonical list"
   end.
 
 Ltac check_fv l :=
   check_is_list l;
-  match type of l with 
+  match type of l with
   | list _ => idtac
-  | _ => fail 100 "anomaly: built an ill-typed list"
+  | _      => fail 100 "anomaly: built an ill-typed list"
   end.
diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v
deleted file mode 100644
index aa2b74dd..00000000
--- a/theories/Lists/MonoList.v
+++ /dev/null
@@ -1,269 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: MonoList.v 8642 2006-03-17 10:09:02Z notin $ i*)
-
-(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
-
-Require Import Le.
-
-Parameter List_Dom : Set.
-Definition A := List_Dom.
-
-Inductive list : Set :=
-  | nil : list
-  | cons : A -> list -> list.
-
-Fixpoint app (l m:list) {struct l} : list :=
-  match l return list with
-  | nil => m
-  | cons a l1 => cons a (app l1 m)
-  end.
-
-
-Lemma app_nil_end : forall l:list, l = app l nil.
-Proof. 
-	intro l; elim l; simpl in |- *; auto.
-        simple induction 1; auto.
-Qed.
-Hint Resolve app_nil_end: list v62.
-
-Lemma app_ass : forall l m n:list, app (app l m) n = app l (app m n).
-Proof. 
-	intros l m n; elim l; simpl in |- *; auto with list.
-	simple induction 1; auto with list.
-Qed.
-Hint Resolve app_ass: list v62.
-
-Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n.
-Proof. 
-	auto with list.
-Qed.
-Hint Resolve ass_app: list v62.
-
-Definition tail (l:list) : list :=
-  match l return list with
-  | cons _ m => m
-  | _ => nil
-  end.
-                   
-
-Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m.
-  intros; discriminate.
-Qed.
-
-(****************************************)
-(* Length of lists                      *)
-(****************************************)
-
-Fixpoint length (l:list) : nat :=
-  match l return nat with
-  | cons _ m => S (length m)
-  | _ => 0
-  end.
-
-(******************************)
-(* Length order of lists      *)
-(******************************)
-
-Section length_order.
-Definition lel (l m:list) := length l <= length m.
-
-Hint Unfold lel: list.
-
-Variables a b : A.
-Variables l m n : list.
-
-Lemma lel_refl : lel l l.
-Proof. 
-	unfold lel in |- *; auto with list.
-Qed.
-
-Lemma lel_trans : lel l m -> lel m n -> lel l n.
-Proof. 
-	unfold lel in |- *; intros.
-        apply le_trans with (length m); auto with list.
-Qed.
-
-Lemma lel_cons_cons : lel l m -> lel (cons a l) (cons b m).
-Proof. 
-	unfold lel in |- *; simpl in |- *; auto with list arith.
-Qed.
-
-Lemma lel_cons : lel l m -> lel l (cons b m).
-Proof. 
-	unfold lel in |- *; simpl in |- *; auto with list arith.
-Qed.
-
-Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m.
-Proof. 
-	unfold lel in |- *; simpl in |- *; auto with list arith.
-Qed.
-
-Lemma lel_nil : forall l':list, lel l' nil -> nil = l'.
-Proof. 
-	intro l'; elim l'; auto with list arith.
-	intros a' y H H0.
-	(*  <list>nil=(cons a' y)
-	    ============================
-	      H0 : (lel (cons a' y) nil)
-	      H : (lel y nil)->(<list>nil=y)
-	      y : list
-	      a' : A
-	      l' : list *)
-	absurd (S (length y) <= 0); auto with list arith.
-Qed.
-End length_order.
-
-Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
-  v62.
-
-Fixpoint In (a:A) (l:list) {struct l} : Prop :=
-  match l with
-  | nil => False
-  | cons b m => b = a \/ In a m
-  end.
-
-Lemma in_eq : forall (a:A) (l:list), In a (cons a l).
-Proof. 
-	simpl in |- *; auto with list.
-Qed.
-Hint Resolve in_eq: list v62.
-
-Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l).
-Proof. 
-	simpl in |- *; auto with list.
-Qed.
-Hint Resolve in_cons: list v62.
-
-Lemma in_app_or : forall (l m:list) (a:A), In a (app l m) -> In a l \/ In a m.
-Proof. 
-	intros l m a.
-	elim l; simpl in |- *; auto with list.
-	intros a0 y H H0.
-	(*  ((<A>a0=a)\/(In a y))\/(In a m)
-	    ============================
-	      H0 : (<A>a0=a)\/(In a (app y m))
-	      H : (In a (app y m))->((In a y)\/(In a m))
-	      y : list
-	      a0 : A
-	      a : A
-	      m : list
-	      l : list *)
-	elim H0; auto with list.
-	intro H1.
-	(*  ((<A>a0=a)\/(In a y))\/(In a m)
-	    ============================
-	      H1 : (In a (app y m)) *)
-	elim (H H1); auto with list.
-Qed.
-Hint Immediate in_app_or: list v62.
-
-Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (app l m).
-Proof. 
-	intros l m a.
-	elim l; simpl in |- *; intro H.
-	(* 1 (In a m)
-	    ============================
-	      H : False\/(In a m)
-	      a : A
-	      m : list
-	      l : list *)
-	elim H; auto with list; intro H0.
-	(*  (In a m)
-	    ============================
-	      H0 : False *)
-	elim H0. (* subProof completed *)
-	intros y H0 H1.
-	(*  2 (<A>H=a)\/(In a (app y m))
-	    ============================
-	      H1 : ((<A>H=a)\/(In a y))\/(In a m)
-	      H0 : ((In a y)\/(In a m))->(In a (app y m))
-	      y : list *)
-	elim H1; auto 4 with list.
-	intro H2.
-	(*  (<A>H=a)\/(In a (app y m))
-	    ============================
-	      H2 : (<A>H=a)\/(In a y) *)
-	elim H2; auto with list.
-Qed.
-Hint Resolve in_or_app: list v62.
-
-Definition incl (l m:list) := forall a:A, In a l -> In a m.
-
-Hint Unfold incl: list v62.
-
-Lemma incl_refl : forall l:list, incl l l.
-Proof. 
-	auto with list.
-Qed.
-Hint Resolve incl_refl: list v62.
-
-Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m).
-Proof. 
-	auto with list.
-Qed.
-Hint Immediate incl_tl: list v62.
-
-Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n.
-Proof. 
-	auto with list.
-Qed.
-
-Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m).
-Proof. 
-	auto with list.
-Qed.
-Hint Immediate incl_appl: list v62.
-
-Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n).
-Proof. 
-	auto with list.
-Qed.
-Hint Immediate incl_appr: list v62.
-
-Lemma incl_cons :
- forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m.
-Proof. 
-	unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
-	(*  (In a0 m)
-	    ============================
-	      H1 : (<A>a=a0)\/(In a0 l)
-	      a0 : A
-	      H0 : (a:A)(In a l)->(In a m)
-	      H : (In a m)
-	      m : list
-	      l : list
-	      a : A *)
-	elim H1.
-	(*  1 (<A>a=a0)->(In a0 m) *)
-	elim H1; auto with list; intro H2.
-	(*  (<A>a=a0)->(In a0 m)
-	    ============================
-	      H2 : <A>a=a0 *)
-	elim H2; auto with list. (* solves subgoal *)
-	(*  2 (In a0 l)->(In a0 m) *)
-	auto with list.
-Qed.
-Hint Resolve incl_cons: list v62.
-
-Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n.
-Proof. 
-	unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
-	(*  (In a n)
-	    ============================
-	      H1 : (In a (app l m))
-	      a : A
-	      H0 : (a:A)(In a m)->(In a n)
-	      H : (a:A)(In a l)->(In a n)
-	      n : list
-	      m : list
-	      l : list *)
-	elim (in_app_or l m a); auto with list.
-Qed.
-Hint Resolve incl_app: list v62.
\ No newline at end of file
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 2592abb5..d42e71e5 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -6,23 +6,23 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: SetoidList.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id$ *)
 
 Require Export List.
 Require Export Sorting.
-Require Export Setoid.
+Require Export Setoid Basics Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** * Logical relations over lists with respect to a setoid equality 
-      or ordering. *) 
+(** * Logical relations over lists with respect to a setoid equality
+      or ordering. *)
 
-(** This can be seen as a complement of predicate [lelistA] and [sort] 
+(** This can be seen as a complement of predicate [lelistA] and [sort]
     found in [Sorting]. *)
 
 Section Type_with_equality.
 Variable A : Type.
-Variable eqA : A -> A -> Prop. 
+Variable eqA : A -> A -> Prop.
 
 (** Being in a list modulo an equality relation over type [A]. *)
 
@@ -32,27 +32,28 @@ Inductive InA (x : A) : list A -> Prop :=
 
 Hint Constructors InA.
 
+(** TODO: it would be nice to have a generic definition instead
+    of the previous one. Having [InA = Exists eqA] raises too
+    many compatibility issues. For now, we only state the equivalence: *)
+
+Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l.
+Proof. split; induction 1; auto. Qed.
+
 Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l.
 Proof.
- intuition.
- inversion H; auto.
+ intuition. invlist InA; auto.
 Qed.
 
 Lemma InA_nil : forall x, InA x nil <-> False.
 Proof.
- intuition.
- inversion H.
+ intuition. invlist InA.
 Qed.
 
 (** An alternative definition of [InA]. *)
 
 Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l.
-Proof. 
- induction l; intuition.
- inversion H.
- firstorder.
- inversion H1; firstorder.
- firstorder; subst; auto.
+Proof.
+ intros; rewrite InA_altdef, Exists_exists; firstorder.
 Qed.
 
 (** A list without redundancy modulo the equality over [A]. *)
@@ -63,8 +64,22 @@ Inductive NoDupA : list A -> Prop :=
 
 Hint Constructors NoDupA.
 
+(** An alternative definition of [NoDupA] based on [ForallOrdPairs] *)
+
+Lemma NoDupA_altdef : forall l,
+ NoDupA l <-> ForallOrdPairs (complement eqA) l.
+Proof.
+ split; induction 1; constructor; auto.
+ rewrite Forall_forall. intros b Hb.
+ intro Eq; elim H. rewrite InA_alt. exists b; auto.
+ rewrite InA_alt; intros (a' & Haa' & Ha').
+ rewrite Forall_forall in H. exact (H a' Ha' Haa').
+Qed.
+
+
 (** lists with same elements modulo [eqA] *)
 
+Definition inclA l l' := forall x, InA x l -> InA x l'.
 Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
 
 (** lists with same elements modulo [eqA] at the same place *)
@@ -76,48 +91,78 @@ Inductive eqlistA : list A -> list A -> Prop :=
 
 Hint Constructors eqlistA.
 
-(** Compatibility of a  boolean function with respect to an equality. *)
+(** We could also have written [eqlistA = Forall2 eqA]. *)
 
-Definition compat_bool (f : A->bool) := forall x y, eqA x y -> f x = f y.
+Lemma eqlistA_altdef : forall l l', eqlistA l l' <-> Forall2 eqA l l'.
+Proof. split; induction 1; auto. Qed.
 
-(** Compatibility of a function upon natural numbers. *)
+(** Results concerning lists modulo [eqA] *)
 
-Definition compat_nat (f : A->nat) := forall x y, eqA x y -> f x = f y.
+Hypothesis eqA_equiv : Equivalence eqA.
 
-(** Compatibility of a predicate with respect to an equality. *)
+Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv).
+Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv).
+Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv).
 
-Definition compat_P (P : A->Prop) := forall x y, eqA x y -> P x -> P y.
+Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
 
-(** Results concerning lists modulo [eqA] *)
+(** First, the two notions [equivlistA] and [eqlistA] are indeed equivlances *)
 
-Hypothesis eqA_refl : forall x, eqA x x.
-Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
-Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
+Global Instance equivlist_equiv : Equivalence equivlistA.
+Proof.
+ firstorder.
+Qed.
+
+Global Instance eqlistA_equiv : Equivalence eqlistA.
+Proof.
+ constructor; red.
+ induction x; auto.
+ induction 1; auto.
+ intros x y z H; revert z; induction H; auto.
+ inversion 1; subst; auto. invlist eqlistA; eauto with *.
+Qed.
+
+(** Moreover, [eqlistA] implies [equivlistA]. A reverse result
+    will be proved later for sorted list without duplicates. *)
+
+Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA.
+Proof.
+  intros x x' H. induction H.
+  intuition.
+  red; intros.
+  rewrite 2 InA_cons.
+  rewrite (IHeqlistA x0), H; intuition.
+Qed.
+
+(** InA is compatible with eqA (for its first arg) and with
+    equivlistA (and hence eqlistA) for its second arg *)
+
+Global Instance InA_compat : Proper (eqA==>equivlistA==>iff) InA.
+Proof.
+ intros x x' Hxx' l l' Hll'. rewrite (Hll' x).
+ rewrite 2 InA_alt; firstorder.
+Qed.
 
-Hint Resolve eqA_refl eqA_trans.
-Hint Immediate eqA_sym.
+(** For compatibility, an immediate consequence of [InA_compat] *)
 
 Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
-Proof. 
- intros s x y.
- do 2 rewrite InA_alt.
- intros H (z,(U,V)).  
- exists z; split; eauto.
+Proof.
+ intros l x y H H'. rewrite <- H; auto.
 Qed.
 Hint Immediate InA_eqA.
 
 Lemma In_InA : forall l x, In x l -> InA x l.
 Proof.
- simple induction l; simpl in |- *; intuition.
- subst; auto.  
+ simple induction l; simpl; intuition.
+ subst; auto.
 Qed.
 Hint Resolve In_InA.
 
-Lemma InA_split : forall l x, InA x l -> 
- exists l1, exists y, exists l2, 
+Lemma InA_split : forall l x, InA x l ->
+ exists l1, exists y, exists l2,
  eqA x y /\ l = l1++y::l2.
 Proof.
-induction l; inversion_clear 1.
+induction l; intros; inv.
 exists (@nil A); exists a; exists l; auto.
 destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))).
 exists (a::l1); exists y; exists l2; auto.
@@ -128,7 +173,7 @@ Lemma InA_app : forall l1 l2 x,
  InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
 Proof.
  induction l1; simpl in *; intuition.
- inversion_clear H; auto.
+ inv; auto.
  elim (IHl1 l2 x H0); auto.
 Qed.
 
@@ -144,7 +189,7 @@ Proof.
  apply in_or_app; auto.
 Qed.
 
-Lemma InA_rev : forall p m, 
+Lemma InA_rev : forall p m,
  InA p (rev m) <-> InA p m.
 Proof.
  intros; do 2 rewrite InA_alt.
@@ -153,107 +198,16 @@ Proof.
  rewrite <- In_rev; auto.
 Qed.
 
-(** Results concerning lists modulo [eqA] and [ltA] *)
-
-Variable ltA : A -> A -> Prop.
 
-Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z.
-Hypothesis ltA_not_eqA : forall x y, ltA x y -> ~ eqA x y.
-Hypothesis ltA_eqA : forall x y z, ltA x y -> eqA y z -> ltA x z.
-Hypothesis eqA_ltA : forall x y z, eqA x y -> ltA y z -> ltA x z.
-
-Hint Resolve ltA_trans.
-Hint Immediate ltA_eqA eqA_ltA.
-
-Notation InfA:=(lelistA ltA).
-Notation SortA:=(sort ltA).
-
-Hint Constructors lelistA sort.
-
-Lemma InfA_ltA :
- forall l x y, ltA x y -> InfA y l -> InfA x l.
-Proof.
- destruct l; constructor; inversion_clear H0; 
- eapply ltA_trans; eauto.
-Qed.
- 
-Lemma InfA_eqA :
- forall l x y, eqA x y -> InfA y l -> InfA x l.
-Proof.
- intro s; case s; constructor; inversion_clear H0; eauto.
-Qed.
-Hint Immediate InfA_ltA InfA_eqA. 
-
-Lemma SortA_InfA_InA :
- forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
-Proof. 
- simple induction l.
- intros; inversion H1.
- intros.
- inversion_clear H0; inversion_clear H1; inversion_clear H2.
- eapply ltA_eqA; eauto.
- eauto.
-Qed.
-  
-Lemma In_InfA :
- forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
-Proof.
- simple induction l; simpl in |- *; intros; constructor; auto.
-Qed.
- 
-Lemma InA_InfA :
- forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
-Proof.
- simple induction l; simpl in |- *; intros; constructor; auto.
-Qed.
-
-(* In fact, this may be used as an alternative definition for InfA: *)
-
-Lemma InfA_alt : 
- forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
-Proof. 
-split.
-intros; eapply SortA_InfA_InA; eauto.
-apply InA_InfA.
-Qed.
-
-Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
-Proof.
- induction l1; simpl; auto.
- inversion_clear 1; auto.
-Qed.
-
-Lemma SortA_app :
- forall l1 l2, SortA l1 -> SortA l2 ->
- (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
- SortA (l1 ++ l2).
-Proof.
- induction l1; simpl in *; intuition.
- inversion_clear H.
- constructor; auto.
- apply InfA_app; auto.
- destruct l2; auto.
-Qed.
 
 Section NoDupA.
 
-Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
-Proof.
- simple induction l; auto.
- intros x l' H H0.
- inversion_clear H0.
- constructor; auto.  
- intro.
- assert (ltA x x) by (eapply SortA_InfA_InA; eauto).
- elim (ltA_not_eqA H3); auto.
-Qed.
-
-Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' -> 
-  (forall x, InA x l -> InA x l' -> False) -> 
+Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' ->
+  (forall x, InA x l -> InA x l' -> False) ->
   NoDupA (l++l').
 Proof.
 induction l; simpl; auto; intros.
-inversion_clear H.
+inv.
 constructor.
 rewrite InA_alt; intros (y,(H4,H5)).
 destruct (in_app_or _ _ _ H5).
@@ -274,35 +228,36 @@ Proof.
 induction l.
 simpl; auto.
 simpl; intros.
-inversion_clear H.
+inv.
 apply NoDupA_app; auto.
 constructor; auto.
-intro H2; inversion H2.
+intro; inv.
 intros x.
 rewrite InA_alt.
 intros (x1,(H2,H3)).
-inversion_clear 1.
+intro; inv.
 destruct H0.
-apply InA_eqA with x1; eauto.
+rewrite <- H4, H2.
 apply In_InA.
 rewrite In_rev; auto.
-inversion H4.
 Qed.
 
 Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
 Proof.
- induction l; simpl in *; inversion_clear 1; auto.
+ induction l; simpl in *; intros; inv; auto.
  constructor; eauto.
  contradict H0.
- rewrite InA_app_iff in *; rewrite InA_cons; intuition.
+ rewrite InA_app_iff in *.
+ rewrite InA_cons.
+ intuition.
 Qed.
 
 Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l').
 Proof.
- induction l; simpl in *; inversion_clear 1; auto.
+ induction l; simpl in *; intros; inv; auto.
  constructor; eauto.
  assert (H2:=IHl _ _ H1).
- inversion_clear H2.
+ inv.
  rewrite InA_cons.
  red; destruct 1.
  apply H0.
@@ -314,287 +269,130 @@ Proof.
  eapply NoDupA_split; eauto.
 Qed.
 
-End NoDupA.
-
-(** Some results about [eqlistA] *)
-
-Section EqlistA.
-
-Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.
-Proof.
-induction 1; auto; simpl; congruence.
-Qed.
-
-Lemma eqlistA_app : forall l1 l1' l2 l2', 
-   eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
-Proof.
-intros l1 l1' l2 l2' H; revert l2 l2'; induction H; simpl; auto.
-Qed.
-
-Lemma eqlistA_rev_app : forall l1 l1', 
-   eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' -> 
-   eqlistA ((rev l1)++l2) ((rev l1')++l2').
-Proof.
-induction 1; auto.
-simpl; intros.
-do 2 rewrite app_ass; simpl; auto.
-Qed.
-
-Lemma eqlistA_rev : forall l1 l1', 
-   eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
-Proof.
-intros.
-rewrite (app_nil_end (rev l1)).
-rewrite (app_nil_end (rev l1')).
-apply eqlistA_rev_app; auto.
-Qed.
-
-Lemma SortA_equivlistA_eqlistA : forall l l', 
-   SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
-Proof.
-induction l; destruct l'; simpl; intros; auto.
-destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.  
-destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.  
-inversion_clear H; inversion_clear H0.
-assert (forall y, InA y l -> ltA a y).
-intros; eapply SortA_InfA_InA with (l:=l); eauto.
-assert (forall y, InA y l' -> ltA a0 y).
-intros; eapply SortA_InfA_InA with (l:=l'); eauto.
-clear H3 H4.
-assert (eqA a a0).
- destruct (H1 a).
- destruct (H1 a0).
- assert (InA a (a0::l')) by auto.
- inversion_clear H8; auto.
- assert (InA a0 (a::l)) by auto.
- inversion_clear H8; auto.
- elim (@ltA_not_eqA a a); auto.
- apply ltA_trans with a0; auto.
-constructor; auto.
-apply IHl; auto.
-split; intros.
-destruct (H1 x).
-assert (H8 : InA x (a0::l')) by auto; inversion_clear H8; auto. 
-elim (@ltA_not_eqA a x); eauto.
-destruct (H1 x).
-assert (H8 : InA x (a::l)) by auto; inversion_clear H8; auto. 
-elim (@ltA_not_eqA a0 x); eauto.
-Qed.
-
-End EqlistA.
-
-(** A few things about [filter] *)
-
-Section Filter.
-
-Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
+Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y ->
+ NoDupA (x::l) -> NoDupA (l1++y::l2) ->
+ equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
 Proof.
-induction l; simpl; auto.
-inversion_clear 1; auto.
-destruct (f a); auto.
-constructor; auto.
-apply In_InfA; auto.
-intros.
-rewrite filter_In in H; destruct H.
-eapply SortA_InfA_InA; eauto.
+ intros; intro a.
+ generalize (H2 a).
+ rewrite !InA_app_iff, !InA_cons.
+ inv.
+ assert (SW:=NoDupA_swap H1). inv.
+ rewrite InA_app_iff in H0.
+ split; intros.
+ assert (~eqA a x) by (contradict H3; rewrite <- H3; auto).
+ assert (~eqA a y) by (rewrite <- H; auto).
+ tauto.
+ assert (OR : eqA a x \/ InA a l) by intuition. clear H6.
+ destruct OR as [EQN|INA]; auto.
+ elim H0.
+ rewrite <-H,<-EQN; auto.
 Qed.
 
-Lemma filter_InA : forall f, (compat_bool f) -> 
- forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
-Proof.
-intros; do 2 rewrite InA_alt; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
-  rewrite (H _ _ H0); auto.
-destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
-  rewrite <- (H _ _ H0); auto.
-Qed.
+End NoDupA.
 
-Lemma filter_split : 
- forall f, (forall x y, f x = true -> f y = false -> ltA x y) -> 
- forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
-Proof.
-induction l; simpl; intros; auto.
-inversion_clear H0.
-pattern l at 1; rewrite IHl; auto.
-case_eq (f a); simpl; intros; auto.
-assert (forall e, In e l -> f e = false).
-  intros.
-  assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)).
-  case_eq (f e); simpl; intros; auto.
-  elim (@ltA_not_eqA e e); auto.
-  apply ltA_trans with a; eauto.
-replace (List.filter f l) with (@nil A); auto.
-generalize H3; clear; induction l; simpl; auto.
-case_eq (f a); auto; intros.
-rewrite H3 in H; auto; try discriminate.
-Qed.
 
-End Filter.
 
 Section Fold.
 
 Variable B:Type.
 Variable eqB:B->B->Prop.
-
-(** Compatibility of a two-argument function with respect to two equalities. *)
-Definition compat_op (f : A -> B -> B) :=
-  forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
-
-(** Two-argument functions that allow to reorder their arguments. *)
-Definition transpose (f : A -> B -> B) :=
-  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). 
-
-(** A version of transpose with restriction on where it should hold *)
-Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
-  forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
-
 Variable st:Equivalence eqB.
 Variable f:A->B->B.
 Variable i:B.
-Variable Comp:compat_op f.
+Variable Comp:Proper (eqA==>eqB==>eqB) f.
 
-Lemma fold_right_eqlistA : 
-   forall s s', eqlistA s s' -> 
+Lemma fold_right_eqlistA :
+   forall s s', eqlistA s s' ->
    eqB (fold_right f i s) (fold_right f i s').
 Proof.
-induction 1; simpl; auto.
-reflexivity.
-Qed.
-
-Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> 
- NoDupA (x::l) -> NoDupA (l1++y::l2) -> 
- equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
-Proof.
- intros; intro a.
- generalize (H2 a).
- repeat rewrite InA_app_iff.
- do 2 rewrite InA_cons.
- inversion_clear H0.
- assert (SW:=NoDupA_swap H1).
- inversion_clear SW.
- rewrite InA_app_iff in H0.
- split; intros.
- assert (~eqA a x).
-  contradict H3; apply InA_eqA with a; auto.
- assert (~eqA a y).
-  contradict H8; eauto.
- intuition.
- assert (eqA a x \/ InA a l) by intuition.
- destruct H8; auto.
- elim H0.
- destruct H7; [left|right]; eapply InA_eqA; eauto.
+induction 1; simpl; auto with relations.
+apply Comp; auto.
 Qed.
 
-(** [ForallList2] : specifies that a certain binary predicate should
-    always hold when inspecting two different elements of the list. *)
-
-Inductive ForallList2 (R : A -> A -> Prop) : list A -> Prop :=
-  | ForallNil : ForallList2 R nil
-  | ForallCons : forall a l,
-     (forall b, In b l -> R a b) ->
-     ForallList2 R l -> ForallList2 R (a::l).
-Hint Constructors ForallList2.
+(** Fold with restricted [transpose] hypothesis. *)
 
-(** [NoDupA] can be written in terms of [ForallList2] *)
-
-Lemma ForallList2_NoDupA : forall l,
- ForallList2 (fun a b => ~eqA a b) l <-> NoDupA l.
-Proof.
- induction l; split; intros; auto.
- inversion_clear H. constructor; [ | rewrite <- IHl; auto ].
- rewrite InA_alt; intros (a',(Haa',Ha')).
- exact (H0 a' Ha' Haa').
- inversion_clear H. constructor; [ | rewrite IHl; auto ].
- intros b Hb.
- contradict H0.
- rewrite InA_alt; exists b; auto.
-Qed.
+Section Fold_With_Restriction.
+Variable R : A -> A -> Prop.
+Hypothesis R_sym : Symmetric R.
+Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.
 
-Lemma ForallList2_impl : forall (R R':A->A->Prop),
- (forall a b, R a b -> R' a b) ->
- forall l, ForallList2 R l -> ForallList2 R' l.
-Proof.
- induction 2; auto.
-Qed.
 
-(** The following definition is easier to use than [ForallList2]. *)
+(*
 
-Definition ForallList2_alt (R:A->A->Prop) l :=
- forall a b, InA a l -> InA b l -> ~eqA a b -> R a b.
+(** [ForallOrdPairs R] is compatible with [equivlistA] over the
+    lists without duplicates, as long as the relation [R]
+    is symmetric and compatible with [eqA]. To prove this fact,
+    we use an auxiliary notion: "forall distinct pairs, ...".
+*)
 
-Section Restriction.
-Variable R : A -> A -> Prop.
+Definition ForallNeqPairs :=
+ ForallPairs (fun a b => ~eqA a b -> R a b).
 
-(** [ForallList2] and [ForallList2_alt] are related, but no completely
+(** [ForallOrdPairs] and [ForallNeqPairs] are related, but not completely
     equivalent. For proving one implication, we need to know that the
     list has no duplicated elements... *)
 
-Lemma ForallList2_equiv1 : forall l, NoDupA l ->
- ForallList2_alt R l -> ForallList2 R l.
+Lemma ForallNeqPairs_ForallOrdPairs : forall l, NoDupA l ->
+ ForallNeqPairs l -> ForallOrdPairs R l.
 Proof.
  induction l; auto.
- constructor. intros b Hb.
- inversion_clear H.
- apply H0; auto.
- contradict H1.
- apply InA_eqA with b; auto.
+ constructor. inv.
+ rewrite Forall_forall; intros b Hb.
+ apply H0; simpl; auto.
+ contradict H1; rewrite H1; auto.
  apply IHl.
- inversion_clear H; auto.
+ inv; auto.
  intros b c Hb Hc Hneq.
- apply H0; auto.
+ apply H0; simpl; auto.
 Qed.
 
 (** ... and for proving the other implication, we need to be able
-   to reverse and adapt relation [R] modulo [eqA]. *)
-
-Hypothesis R_sym : forall a b, R a b -> R b a.
-Hypothesis R_compat : forall a, compat_P (R a).
+   to reverse relation [R]. *)
 
-Lemma ForallList2_equiv2 : forall l,
- ForallList2 R l -> ForallList2_alt R l.
+Lemma ForallOrdPairs_ForallNeqPairs : forall l,
+ ForallOrdPairs R l -> ForallNeqPairs l.
 Proof.
- induction l.
- intros _. red. intros a b Ha. inversion Ha.
- inversion_clear 1 as [|? ? H_R Hl].
- intros b c Hb Hc Hneq.
- inversion_clear Hb; inversion_clear Hc.
- (* b,c = a : impossible *)
- elim Hneq; eauto.
- (* b = a, c in l *)
- rewrite InA_alt in H0; destruct H0 as (d,(Hcd,Hd)).
- apply R_compat with d; auto.
- apply R_sym; apply R_compat with a; auto.
- (* b in l, c = a *)
- rewrite InA_alt in H; destruct H as (d,(Hcd,Hd)).
- apply R_compat with a; auto.
- apply R_sym; apply R_compat with d; auto.
- (* b,c in l *)
- apply (IHl Hl); auto.
+ intros l Hl x y Hx Hy N.
+ destruct (ForallOrdPairs_In Hl x y Hx Hy) as [H|[H|H]].
+ subst; elim N; auto.
+ assumption.
+ apply R_sym; assumption.
 Qed.
 
-Lemma ForallList2_equiv : forall l, NoDupA l ->
- (ForallList2 R l <-> ForallList2_alt R l).
-Proof.
-split; [apply ForallList2_equiv2|apply ForallList2_equiv1]; auto.
-Qed.
+*)
+
+(** Compatibility of [ForallOrdPairs] with respect to [inclA]. *)
 
-Lemma ForallList2_equivlistA : forall l l', NoDupA l' ->
- equivlistA l l' -> ForallList2 R l -> ForallList2 R l'.
+Lemma ForallOrdPairs_inclA : forall l l',
+ NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'.
 Proof.
-intros.
-apply ForallList2_equiv1; auto.
-intros a b Ha Hb Hneq.
-red in H0; rewrite <- H0 in Ha,Hb.
-revert a b Ha Hb Hneq.
-change (ForallList2_alt R l).
-apply ForallList2_equiv2; auto.
+induction l' as [|x l' IH].
+constructor.
+intros ND Incl FOP. apply FOP_cons; inv; unfold inclA in *; auto.
+rewrite Forall_forall; intros y Hy.
+assert (Ix : InA x (x::l')) by (rewrite InA_cons; auto).
+ apply Incl in Ix. rewrite InA_alt in Ix. destruct Ix as (x' & Hxx' & Hx').
+assert (Iy : InA y (x::l')) by (apply In_InA; simpl; auto).
+ apply Incl in Iy. rewrite InA_alt in Iy. destruct Iy as (y' & Hyy' & Hy').
+rewrite Hxx', Hyy'.
+destruct (ForallOrdPairs_In FOP x' y' Hx' Hy') as [E|[?|?]]; auto.
+absurd (InA x l'); auto. rewrite Hxx', E, <- Hyy'; auto.
 Qed.
 
+
+(** Two-argument functions that allow to reorder their arguments. *)
+Definition transpose (f : A -> B -> B) :=
+  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
+
+(** A version of transpose with restriction on where it should hold *)
+Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
+  forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
+
 Variable TraR :transpose_restr R f.
 
 Lemma fold_right_commutes_restr :
-  forall s1 s2 x, ForallList2 R (s1++x::s2) ->
+  forall s1 s2 x, ForallOrdPairs R (s1++x::s2) ->
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
 Proof.
 induction s1; simpl; auto; intros.
@@ -602,15 +400,15 @@ reflexivity.
 transitivity (f a (f x (fold_right f i (s1++s2)))).
 apply Comp; auto.
 apply IHs1.
-inversion_clear H; auto.
+invlist ForallOrdPairs; auto.
 apply TraR.
-inversion_clear H.
-apply H0.
+invlist ForallOrdPairs; auto.
+rewrite Forall_forall in H0; apply H0.
 apply in_or_app; simpl; auto.
 Qed.
 
 Lemma fold_right_equivlistA_restr :
-  forall s s', NoDupA s -> NoDupA s' -> ForallList2 R s ->
+  forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
 Proof.
  simple induction s.
@@ -618,35 +416,35 @@ Proof.
  intros; reflexivity.
  unfold equivlistA; intros.
  destruct (H2 a).
- assert (X : InA a nil); auto; inversion X.
+ assert (InA a nil) by auto; inv.
  intros x l Hrec s' N N' F E; simpl in *.
- assert (InA x s').
-  rewrite <- (E x); auto.
+ assert (InA x s') by (rewrite <- (E x); auto).
  destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
  subst s'.
  transitivity (f x (fold_right f i (s1++s2))).
  apply Comp; auto.
  apply Hrec; auto.
- inversion_clear N; auto.
+ inv; auto.
  eapply NoDupA_split; eauto.
- inversion_clear F; auto.
+ invlist ForallOrdPairs; auto.
  eapply equivlistA_NoDupA_split; eauto.
  transitivity (f y (fold_right f i (s1++s2))).
  apply Comp; auto. reflexivity.
  symmetry; apply fold_right_commutes_restr.
- apply ForallList2_equivlistA with (x::l); auto.
+ apply ForallOrdPairs_inclA with (x::l); auto.
+  red; intros; rewrite E; auto.
 Qed.
 
 Lemma fold_right_add_restr :
-  forall s' s x, NoDupA s -> NoDupA s' -> ForallList2 R s' -> ~ InA x s ->
+  forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
 Proof.
  intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto.
 Qed.
 
-End Restriction.
+End Fold_With_Restriction.
 
-(** we know state similar results, but without restriction on transpose. *)
+(** we now state similar results, but without restriction on transpose. *)
 
 Variable Tra :transpose f.
 
@@ -656,6 +454,7 @@ Proof.
 induction s1; simpl; auto; intros.
 reflexivity.
 transitivity (f a (f x (fold_right f i (s1++s2)))); auto.
+apply Comp; auto.
 Qed.
 
 Lemma fold_right_equivlistA :
@@ -663,8 +462,8 @@ Lemma fold_right_equivlistA :
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
 Proof.
 intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True);
- try red; auto.
-apply ForallList2_equiv1; try red; auto.
+ repeat red; auto.
+apply ForallPairs_ForallOrdPairs; try red; auto.
 Qed.
 
 Lemma fold_right_add :
@@ -674,6 +473,8 @@ Proof.
  intros; apply (@fold_right_equivlistA s' (x::s)); auto.
 Qed.
 
+End Fold.
+
 Section Remove.
 
 Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
@@ -682,15 +483,15 @@ Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }.
 Proof.
 induction l.
 right; auto.
-red; inversion 1.
+intro; inv.
 destruct (eqA_dec x a).
 left; auto.
 destruct IHl.
 left; auto.
-right; red; inversion_clear 1; contradiction. 
-Qed.
+right; intro; inv; contradiction.
+Defined.
 
-Fixpoint removeA (x : A) (l : list A){struct l} : list A :=
+Fixpoint removeA (x : A) (l : list A) : list A :=
   match l with
     | nil => nil
     | y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl)
@@ -708,21 +509,21 @@ Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
 Proof.
 induction l; simpl; auto.
 split.
-inversion_clear 1.
-destruct 1; inversion_clear H.
+intro; inv.
+destruct 1; inv.
 intros.
 destruct (eqA_dec x a); simpl; auto.
 rewrite IHl; split; destruct 1; split; auto.
-inversion_clear H; auto.
-destruct H0; apply eqA_trans with a; auto.
+inv; auto.
+destruct H0; transitivity a; auto.
 split.
-inversion_clear 1.
+intro; inv.
 split; auto.
 contradict n.
-apply eqA_trans with y; auto.
+transitivity y; auto.
 rewrite (IHl x y) in H0; destruct H0; auto.
-destruct 1; inversion_clear H; auto.
-constructor 2; rewrite IHl; auto.
+destruct 1; inv; auto.
+right; rewrite IHl; auto.
 Qed.
 
 Lemma removeA_NoDupA :
@@ -730,17 +531,17 @@ Lemma removeA_NoDupA :
 Proof.
 simple induction s; simpl; intros.
 auto.
-inversion_clear H0.
-destruct (eqA_dec x a); simpl; auto. 
+inv.
+destruct (eqA_dec x a); simpl; auto.
 constructor; auto.
 rewrite removeA_InA.
 intuition.
-Qed. 
+Qed.
 
-Lemma removeA_equivlistA : forall l l' x, 
+Lemma removeA_equivlistA : forall l l' x,
   ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
-Proof.  
-unfold equivlistA; intros. 
+Proof.
+unfold equivlistA; intros.
 rewrite removeA_InA.
 split; intros.
 rewrite <- H0; split; auto.
@@ -748,64 +549,306 @@ contradict H.
 apply InA_eqA with x0; auto.
 rewrite <- (H0 x0) in H1.
 destruct H1.
-inversion_clear H1; auto.
+inv; auto.
 elim H2; auto.
 Qed.
 
 End Remove.
 
-End Fold.
 
+
+(** Results concerning lists modulo [eqA] and [ltA] *)
+
+Variable ltA : A -> A -> Prop.
+Hypothesis ltA_strorder : StrictOrder ltA.
+Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
+
+Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder).
+
+Notation InfA:=(lelistA ltA).
+Notation SortA:=(sort ltA).
+
+Hint Constructors lelistA sort.
+
+Lemma InfA_ltA :
+ forall l x y, ltA x y -> InfA y l -> InfA x l.
+Proof.
+ destruct l; constructor. inv; eauto.
+Qed.
+
+Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA.
+Proof.
+ intros x x' Hxx' l l' Hll'.
+ inversion_clear Hll'.
+ intuition.
+ split; intro; inv; constructor.
+ rewrite <- Hxx', <- H; auto.
+ rewrite Hxx', H; auto.
+Qed.
+
+(** For compatibility, can be deduced from [InfA_compat] *)
+Lemma InfA_eqA :
+ forall l x y, eqA x y -> InfA y l -> InfA x l.
+Proof.
+ intros l x y H; rewrite H; auto.
+Qed.
+Hint Immediate InfA_ltA InfA_eqA.
+
+Lemma SortA_InfA_InA :
+ forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
+Proof.
+ simple induction l.
+ intros. inv.
+ intros. inv.
+ setoid_replace x with a; auto.
+ eauto.
+Qed.
+
+Lemma In_InfA :
+ forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
+Proof.
+ simple induction l; simpl; intros; constructor; auto.
+Qed.
+
+Lemma InA_InfA :
+ forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
+Proof.
+ simple induction l; simpl; intros; constructor; auto.
+Qed.
+
+(* In fact, this may be used as an alternative definition for InfA: *)
+
+Lemma InfA_alt :
+ forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
+Proof.
+split.
+intros; eapply SortA_InfA_InA; eauto.
+apply InA_InfA.
+Qed.
+
+Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
+Proof.
+ induction l1; simpl; auto.
+ intros; inv; auto.
+Qed.
+
+Lemma SortA_app :
+ forall l1 l2, SortA l1 -> SortA l2 ->
+ (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
+ SortA (l1 ++ l2).
+Proof.
+ induction l1; simpl in *; intuition.
+ inv.
+ constructor; auto.
+ apply InfA_app; auto.
+ destruct l2; auto.
+Qed.
+
+Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
+Proof.
+ simple induction l; auto.
+ intros x l' H H0.
+ inv.
+ constructor; auto.
+ intro.
+ apply (StrictOrder_Irreflexive x).
+ eapply SortA_InfA_InA; eauto.
+Qed.
+
+
+(** Some results about [eqlistA] *)
+
+Section EqlistA.
+
+Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.
+Proof.
+induction 1; auto; simpl; congruence.
+Qed.
+
+Global Instance app_eqlistA_compat :
+ Proper (eqlistA==>eqlistA==>eqlistA) (@app A).
+Proof.
+ repeat red; induction 1; simpl; auto.
+Qed.
+
+(** For compatibility, can be deduced from app_eqlistA_compat **)
+Lemma eqlistA_app : forall l1 l1' l2 l2',
+   eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
+Proof.
+intros l1 l1' l2 l2' H H'; rewrite H, H'; reflexivity.
+Qed.
+
+Lemma eqlistA_rev_app : forall l1 l1',
+   eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' ->
+   eqlistA ((rev l1)++l2) ((rev l1')++l2').
+Proof.
+induction 1; auto.
+simpl; intros.
+do 2 rewrite app_ass; simpl; auto.
+Qed.
+
+Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A).
+Proof.
+repeat red. intros.
+rewrite (app_nil_end (rev x)), (app_nil_end (rev y)).
+apply eqlistA_rev_app; auto.
+Qed.
+
+Lemma eqlistA_rev : forall l1 l1',
+   eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
+Proof.
+apply rev_eqlistA_compat.
+Qed.
+
+Lemma SortA_equivlistA_eqlistA : forall l l',
+   SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
+Proof.
+induction l; destruct l'; simpl; intros; auto.
+destruct (H1 a); assert (InA a nil) by auto; inv.
+destruct (H1 a); assert (InA a nil) by auto; inv.
+inv.
+assert (forall y, InA y l -> ltA a y).
+intros; eapply SortA_InfA_InA with (l:=l); eauto.
+assert (forall y, InA y l' -> ltA a0 y).
+intros; eapply SortA_InfA_InA with (l:=l'); eauto.
+clear H3 H4.
+assert (eqA a a0).
+ destruct (H1 a).
+ destruct (H1 a0).
+ assert (InA a (a0::l')) by auto. inv; auto.
+ assert (InA a0 (a::l)) by auto. inv; auto.
+ elim (StrictOrder_Irreflexive a); eauto.
+constructor; auto.
+apply IHl; auto.
+split; intros.
+destruct (H1 x).
+assert (InA x (a0::l')) by auto. inv; auto.
+rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto.
+destruct (H1 x).
+assert (InA x (a::l)) by auto. inv; auto.
+rewrite H9,H3 in H4. elim (StrictOrder_Irreflexive a0); eauto.
+Qed.
+
+End EqlistA.
+
+(** A few things about [filter] *)
+
+Section Filter.
+
+Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
+Proof.
+induction l; simpl; auto.
+intros; inv; auto.
+destruct (f a); auto.
+constructor; auto.
+apply In_InfA; auto.
+intros.
+rewrite filter_In in H; destruct H.
+eapply SortA_InfA_InA; eauto.
+Qed.
+
+Implicit Arguments eq [ [A] ].
+
+Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
+ forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
+Proof.
+clear ltA ltA_compat ltA_strorder.
+intros; do 2 rewrite InA_alt; intuition.
+destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
+destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
+  rewrite (H _ _ H0); auto.
+destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
+  rewrite <- (H _ _ H0); auto.
+Qed.
+
+Lemma filter_split :
+ forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
+ forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
+Proof.
+induction l; simpl; intros; auto.
+inv.
+rewrite IHl at 1; auto.
+case_eq (f a); simpl; intros; auto.
+assert (forall e, In e l -> f e = false).
+  intros.
+  assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)).
+  case_eq (f e); simpl; intros; auto.
+  elim (StrictOrder_Irreflexive e).
+  transitivity a; auto.
+replace (List.filter f l) with (@nil A); auto.
+generalize H3; clear; induction l; simpl; auto.
+case_eq (f a); auto; intros.
+rewrite H3 in H; auto; try discriminate.
+Qed.
+
+End Filter.
 End Type_with_equality.
 
-Hint Unfold compat_bool compat_nat compat_P.
-Hint Constructors InA NoDupA sort lelistA eqlistA.
 
-Section Find. 
-Variable A B : Type. 
-Variable eqA : A -> A -> Prop. 
-Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
-Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
+Hint Constructors InA eqlistA NoDupA sort lelistA.
+
+Section Find.
+
+Variable A B : Type.
+Variable eqA : A -> A -> Prop.
+Hypothesis eqA_equiv : Equivalence eqA.
 Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
 
-Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B := 
- match l with  
-  | nil => None 
+Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B :=
+ match l with
+  | nil => None
   | (a,b)::l => if f a then Some b else findA f l
  end.
 
-Lemma findA_NoDupA : 
- forall l a b, 
- NoDupA (fun p p' => eqA (fst p) (fst p')) l -> 
+Lemma findA_NoDupA :
+ forall l a b,
+ NoDupA (fun p p' => eqA (fst p) (fst p')) l ->
  (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (a,b) l <->
   findA (fun a' => if eqA_dec a a' then true else false) l = Some b).
 Proof.
-induction l; simpl; intros.
+set (eqk := fun p p' : A*B => eqA (fst p) (fst p')).
+set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p').
+induction l; intros; simpl.
 split; intros; try discriminate.
-inversion H0.
+invlist InA.
 destruct a as (a',b'); rename a0 into a.
-inversion_clear H.
+invlist NoDupA.
 split; intros.
-inversion_clear H.
-simpl in *; destruct H2; subst b'.
+invlist InA.
+compute in H2; destruct H2. subst b'.
 destruct (eqA_dec a a'); intuition.
 destruct (eqA_dec a a'); simpl.
-destruct H0.
-generalize e H2 eqA_trans eqA_sym; clear.
+contradict H0.
+revert e H2; clear - eqA_equiv.
 induction l.
-inversion 2.
-inversion_clear 2; intros; auto.
+intros; invlist InA.
+intros; invlist InA; auto.
 destruct a0.
 compute in H; destruct H.
 subst b.
-constructor 1; auto.
-simpl.
-apply eqA_trans with a; auto.
+left; auto.
+compute.
+transitivity a; auto. symmetry; auto.
 rewrite <- IHl; auto.
 destruct (eqA_dec a a'); simpl in *.
-inversion H; clear H; intros; subst b'; auto.
-constructor 2.
-rewrite IHl; auto.
+left; split; simpl; congruence.
+right. rewrite IHl; auto.
 Qed.
 
-End Find. 
+End Find.
+
+
+(** Compatibility aliases. [Proper] is rather to be used directly now.*)
+
+Definition compat_bool {A} (eqA:A->A->Prop)(f:A->bool) :=
+ Proper (eqA==>Logic.eq) f.
+
+Definition compat_nat {A} (eqA:A->A->Prop)(f:A->nat) :=
+ Proper (eqA==>Logic.eq) f.
+
+Definition compat_P {A} (eqA:A->A->Prop)(P:A->Prop) :=
+ Proper (eqA==>impl) P.
+
+Definition compat_op {A B} (eqA:A->A->Prop)(eqB:B->B->Prop)(f:A->B->B) :=
+ Proper (eqA==>eqB==>eqB) f.
+
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index bdbe0ecc..d906cfa4 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -11,8 +11,8 @@ Require Import Streams.
 
 (** * Memoization *)
 
-(** Successive outputs of a given function [f] are stored in 
-    a stream in order to avoid duplicated computations. *) 
+(** Successive outputs of a given function [f] are stored in
+    a stream in order to avoid duplicated computations. *)
 
 Section MemoFunction.
 
@@ -24,8 +24,8 @@ CoFixpoint memo_make (n:nat) : Stream A := Cons (f n) (memo_make (S n)).
 Definition memo_list := memo_make 0.
 
 Fixpoint memo_get (n:nat) (l:Stream A) : A :=
-  match n with 
-    | O => hd l 
+  match n with
+    | O => hd l
     | S n1 => memo_get n1 (tl l)
   end.
 
@@ -49,7 +49,7 @@ Variable g: A -> A.
 Hypothesis Hg_correct: forall n, f (S n) = g (f n).
 
 CoFixpoint imemo_make (fn:A) : Stream A :=
-  let fn1 := g fn in 
+  let fn1 := g fn in
   Cons fn1 (imemo_make fn1).
 
 Definition imemo_list := let f0 := f 0 in
@@ -68,7 +68,7 @@ Qed.
 
 End MemoFunction.
 
-(** For a dependent function, the previous solution is 
+(** For a dependent function, the previous solution is
     reused thanks to a temporarly hiding of the dependency
     in a "container" [memo_val]. *)
 
@@ -80,7 +80,7 @@ Variable f: forall n, A n.
 Inductive memo_val: Type :=
   memo_mval: forall n, A n -> memo_val.
 
-Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} :=
+Fixpoint is_eq (n m : nat) : {n = m} + {True} :=
   match n, m return {n = m} + {True} with
   | 0, 0 =>left True (refl_equal 0)
   | 0, S m1 => right (0 = S m1) I
@@ -88,7 +88,7 @@ Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} :=
   | S n1, S m1 =>
      match is_eq n1 m1 with
      | left H => left True (f_equal S H)
-     | right _ => right (S n1 = S m1) I 
+     | right _ => right (S n1 = S m1) I
      end
   end.
 
@@ -97,7 +97,7 @@ match v with
 | memo_mval m x =>
     match is_eq n m with
     | left H =>
-       match H in (@eq _ _ y) return (A y -> A n) with
+       match H in (eq _ y) return (A y -> A n) with
         | refl_equal => fun v1 : A n => v1
        end
     | right _ => fun _ : A m => f n
@@ -134,7 +134,7 @@ Variable g: forall n, A n -> A (S n).
 
 Hypothesis Hg_correct: forall n, f (S n) = g n (f n).
 
-Let mg v :=  match v with 
+Let mg v :=  match v with
              memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end.
 
 Definition dimemo_list := imemo_list _ mf mg.
@@ -166,13 +166,13 @@ End DependentMemoFunction.
 Require Import ZArith.
 Open Scope Z_scope.
 
-Fixpoint tfact (n: nat) := 
-  match n with 
-   | O => 1 
-   | S n1 => Z_of_nat n * tfact n1 
+Fixpoint tfact (n: nat) :=
+  match n with
+   | O => 1
+   | S n1 => Z_of_nat n * tfact n1
   end.
 
-Definition lfact_list := 
+Definition lfact_list :=
   dimemo_list _ tfact (fun n z => (Z_of_nat (S  n) * z)).
 
 Definition lfact n := dmemo_get _ tfact n lfact_list.
@@ -183,18 +183,18 @@ intros n; unfold lfact, lfact_list.
 rewrite dimemo_get_correct; auto.
 Qed.
 
-Fixpoint nop p := 
+Fixpoint nop p :=
   match p with
-   | xH => 0 
-   | xI p1 => nop p1 
-   | xO p1 => nop p1 
+   | xH => 0
+   | xI p1 => nop p1
+   | xO p1 => nop p1
   end.
 
-Fixpoint test z := 
+Fixpoint test z :=
   match z with
-   | Z0 => 0 
-   | Zpos p1 => nop p1 
-   | Zneg p1 => nop p1 
+   | Z0 => 0
+   | Zpos p1 => nop p1
+   | Zneg p1 => nop p1
   end.
 
 Time Eval vm_compute in test (lfact 2000).
@@ -202,4 +202,4 @@ Time Eval vm_compute in test (lfact 2000).
 Time Eval vm_compute in test (lfact 1500).
 Time Eval vm_compute in (lfact 1500).
 *)
- 
+
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 49990502..3fa053b7 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Streams.v 9967 2007-07-11 15:25:03Z roconnor $ i*)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
@@ -29,7 +29,7 @@ Definition tl (x:Stream) := match x with
                             end.
 
 
-Fixpoint Str_nth_tl (n:nat) (s:Stream) {struct n} : Stream :=
+Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream :=
   match n with
   | O => s
   | S m => Str_nth_tl m (tl s)
@@ -41,7 +41,7 @@ Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s).
 Lemma unfold_Stream :
  forall x:Stream, x = match x with
                       | Cons a s => Cons a s
-                      end. 
+                      end.
 Proof.
   intro x.
   case x.
@@ -223,7 +223,7 @@ Variable f: A -> B -> C.
 CoFixpoint zipWith (a:Stream A) (b:Stream B) : Stream C :=
 Cons (f (hd a) (hd b)) (zipWith (tl a) (tl b)).
 
-Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B), 
+Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B),
  Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b).
 Proof.
 induction n.
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 2bfb70fe..7ed9c519 100644
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -6,12 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: TheoryList.v 8866 2006-05-28 16:21:04Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** Some programs and results about lists following CAML Manual *)
 
 Require Export List.
 Set Implicit Arguments.
+
+Local Notation "[ ]" := nil (at level 0).
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).
+
 Section Lists.
 
 Variable A : Type.
@@ -23,11 +27,13 @@ Variable A : Type.
 Definition Isnil (l:list A) : Prop := nil = l.
 
 Lemma Isnil_nil : Isnil nil.
+Proof.
 red in |- *; auto.
 Qed.
 Hint Resolve Isnil_nil.
 
 Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l).
+Proof.
 unfold Isnil in |- *.
 intros; discriminate.
 Qed.
@@ -35,6 +41,7 @@ Qed.
 Hint Resolve Isnil_nil not_Isnil_cons.
 
 Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}.
+Proof.
 intro l; case l; auto.
 (*
 Realizer (fun l => match l with
@@ -50,6 +57,7 @@ Qed.
 
 Lemma Uncons :
  forall l:list A, {a : A &  {m : list A | a :: m = l}} + {Isnil l}.
+Proof.
 intro l; case l.
 auto.
 intros a m; intros; left; exists a; exists m; reflexivity.
@@ -67,6 +75,7 @@ Qed.
 
 Lemma Hd :
  forall l:list A, {a : A |  exists m : list A, a :: m = l} + {Isnil l}.
+Proof.
 intro l; case l.
 auto.
 intros a m; intros; left; exists a; exists m; reflexivity.
@@ -81,6 +90,7 @@ Qed.
 Lemma Tl :
  forall l:list A,
    {m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}.
+Proof.
 intro l; case l.
 exists (nil (A:=A)); auto.
 intros a m; intros; exists m; left; exists a; reflexivity.
@@ -97,7 +107,7 @@ Qed.
 (****************************************)
 
 (* length is defined in List *)
-Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat :=
+Fixpoint Length_l (l:list A) (n:nat) : nat :=
   match l with
   | nil => n
   | _ :: m => Length_l m (S n)
@@ -105,6 +115,7 @@ Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat :=
 
 (* A tail recursive version *)
 Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}.
+Proof.
 induction l as [| a m lrec].
 intro n; exists n; simpl in |- *; auto.
 intro n; elim (lrec (S n)); simpl in |- *; intros.
@@ -115,6 +126,7 @@ Realizer Length_l.
 Qed.
 
 Lemma Length : forall l:list A, {m : nat | length l = m}.
+Proof.
 intro l. apply (Length_l_pf l 0).
 (*
 Realizer (fun l -> Length_l_pf l O).
@@ -139,14 +151,9 @@ elim l;
 intros; elim H; auto.
 Qed.
 
-Inductive AllS (P:A -> Prop) : list A -> Prop :=
-  | allS_nil : AllS P nil
-  | allS_cons : forall (a:A) (l:list A), P a -> AllS P l -> AllS P (a :: l).
-Hint Resolve allS_nil allS_cons.
-
 Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}.
 
-Fixpoint mem (a:A) (l:list A) {struct l} : bool :=
+Fixpoint mem (a:A) (l:list A) : bool :=
   match l with
   | nil => false
   | b :: m => if eqA_dec a b then true else mem a m
@@ -154,7 +161,7 @@ Fixpoint mem (a:A) (l:list A) {struct l} : bool :=
 
 Hint Unfold In.
 Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}.
-intros a l.
+Proof.
 induction l.
 auto.
 elim (eqA_dec a a0).
@@ -188,20 +195,23 @@ Hint Resolve fst_nth_O fst_nth_S.
 
 Lemma fst_nth_nth :
  forall (l:list A) (n:nat) (a:A), fst_nth_spec l n a -> nth_spec l n a.
+Proof.
 induction 1; auto.
 Qed.
 Hint Immediate fst_nth_nth.
 
 Lemma nth_lt_O : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> 0 < n.
+Proof.
 induction 1; auto.
 Qed.
 
 Lemma nth_le_length :
  forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l.
+Proof.
 induction 1; simpl in |- *; auto with arith.
 Qed.
 
-Fixpoint Nth_func (l:list A) (n:nat) {struct l} : Exc A :=
+Fixpoint Nth_func (l:list A) (n:nat) : Exc A :=
   match l, n with
   | a :: _, S O => value a
   | _ :: l', S (S p) => Nth_func l' (S p)
@@ -211,6 +221,7 @@ Fixpoint Nth_func (l:list A) (n:nat) {struct l} : Exc A :=
 Lemma Nth :
  forall (l:list A) (n:nat),
    {a : A | nth_spec l n a} + {n = 0 \/ length l < n}.
+Proof.
 induction l as [| a l IHl].
 intro n; case n; simpl in |- *; auto with arith.
 intro n; destruct n as [| [| n1]]; simpl in |- *; auto.
@@ -227,6 +238,7 @@ Qed.
 
 Lemma Item :
  forall (l:list A) (n:nat), {a : A | nth_spec l (S n) a} + {length l <= n}.
+Proof.
 intros l n; case (Nth l (S n)); intro.
 case s; intro a; left; exists a; auto.
 right; case o; intro.
@@ -237,7 +249,7 @@ Qed.
 Require Import Minus.
 Require Import DecBool.
 
-Fixpoint index_p (a:A) (l:list A) {struct l} : nat -> Exc nat :=
+Fixpoint index_p (a:A) (l:list A) : nat -> Exc nat :=
   match l with
   | nil => fun p => error
   | b :: m => fun p => ifdec (eqA_dec a b) (value p) (index_p a m (S p))
@@ -246,6 +258,7 @@ Fixpoint index_p (a:A) (l:list A) {struct l} : nat -> Exc nat :=
 Lemma Index_p :
  forall (a:A) (l:list A) (p:nat),
    {n : nat | fst_nth_spec l (S n - p) a} + {AllS (fun b:A => a <> b) l}.
+Proof.
 induction l as [| b m irec].
 auto.
 intro p.
@@ -264,6 +277,7 @@ Lemma Index :
  forall (a:A) (l:list A),
    {n : nat | fst_nth_spec l n a} + {AllS (fun b:A => a <> b) l}.
 
+Proof.
 intros a l; case (Index_p a l 1); auto.
 intros [n P]; left; exists n; auto.
 rewrite (minus_n_O n); trivial.
@@ -287,20 +301,24 @@ Definition InR_inv (l:list A) :=
   end.
 
 Lemma InR_INV : forall l:list A, InR l -> InR_inv l.
+Proof.
 induction 1; simpl in |- *; auto.
 Qed.
 
 Lemma InR_cons_inv : forall (a:A) (l:list A), InR (a :: l) -> R a \/ InR l.
+Proof.
 intros a l H; exact (InR_INV H).
 Qed.
 
 Lemma InR_or_app : forall l m:list A, InR l \/ InR m -> InR (l ++ m).
+Proof.
 intros l m [| ].
 induction 1; simpl in |- *; auto.
 intro. induction l; simpl in |- *; auto.
 Qed.
 
 Lemma InR_app_or : forall l m:list A, InR (l ++ m) -> InR l \/ InR m.
+Proof.
 intros l m; elim l; simpl in |- *; auto.
 intros b l' Hrec IAc; elim (InR_cons_inv IAc); auto.
 intros; elim Hrec; auto.
@@ -315,6 +333,7 @@ Fixpoint find (l:list A) : Exc A :=
   end.
 
 Lemma Find : forall l:list A, {a : A | In a l &  R a} + {AllS P l}.
+Proof.
 induction l as [| a m [[b H1 H2]| H]]; auto.
 left; exists b; auto.
 destruct (RS_dec a).
@@ -342,6 +361,7 @@ Fixpoint try_find (l:list A) : Exc B :=
 
 Lemma Try_find :
  forall l:list A, {c : B |  exists2 a : A, In a l & T a c} + {AllS P l}.
+Proof.
 induction l as [| a m [[b H1]| H]].
 auto.
 left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto.
@@ -349,7 +369,7 @@ destruct (TS_dec a) as [[c H1]| ].
 left; exists c.
 exists a; auto.
 auto.
-(* 
+(*
 Realizer try_find.
 *)
 Qed.
@@ -359,7 +379,7 @@ End Find_sec.
 Section Assoc_sec.
 
 Variable B : Type.
-Fixpoint assoc (a:A) (l:list (A * B)) {struct l} : 
+Fixpoint assoc (a:A) (l:list (A * B)) :
  Exc B :=
   match l with
   | nil => error
@@ -383,6 +403,7 @@ Hint Resolve allS_assoc_nil allS_assoc_cons.
 
 Lemma Assoc :
  forall (a:A) (l:list (A * B)), B + {AllS_assoc (fun a':A => a <> a') l}.
+Proof.
 induction l as [| [a' b] m assrec]. auto.
 destruct (eqA_dec a a').
 left; exact b.
@@ -398,6 +419,5 @@ End Assoc_sec.
 
 End Lists.
 
-Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons:
-  datatypes.
+Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons : datatypes.
 Hint Immediate fst_nth_nth: datatypes.
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
index c45f8803..0051e2c2 100755
--- a/theories/Lists/intro.tex
+++ b/theories/Lists/intro.tex
@@ -21,7 +21,4 @@ This library includes the following files:
   coinductive type. Basic facts are stated and proved. The streams are
   also polymorphic.
 
-\item {\tt MonoList.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
-  WITH OLDER VERSIONS OF COQ. THE USER SHOULD USE {\tt List.v} INSTEAD.
-
 \end{itemize}
diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget
new file mode 100644
index 00000000..d2a31367
--- /dev/null
+++ b/theories/Lists/vo.itarget
@@ -0,0 +1,7 @@
+ListSet.vo
+ListTactics.vo
+List.vo
+SetoidList.vo
+StreamMemo.vo
+Streams.vo
+TheoryList.vo