Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

7 files changed, 1234 insertions, 1454 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 7e6cf4c880..1eb095c149 100755
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -8,254 +8,643 @@
 
 (*i $Id$ i*)
 
-(* This file is a copy of file MonoList.v *)
+Require Import Le.
 
-(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
 
-Require Le.
+Section Lists.
 
-Parameter List_Dom:Set.
-Definition A := List_Dom.
+Variable A : Set.
 
-Inductive list : Set := nil : list | cons : A -> list -> list.
+Set Implicit Arguments.
 
-Fixpoint app [l:list] : list -> list 
-      := [m:list]<list>Cases l of
-                           nil =>  m 
-                       | (cons a l1) => (cons a (app l1 m)) 
-                   end.
+Inductive list : Set :=
+  | nil : list
+  | cons : A -> list -> list.
 
+Infix "::" := cons (at level 60, right associativity) : list_scope.
 
-Lemma app_nil_end : (l:list)(l=(app l nil)).
+Open Scope list_scope.
+
+(*************************)
+(** Discrimination       *)
+(*************************)
+
+Lemma nil_cons : forall (a:A) (m:list), nil <> a :: m.
 Proof. 
-	Intro l ; Elim l ; Simpl ; Auto.
-        Induction 1; Auto.
+  intros; discriminate.
 Qed.
-Hints Resolve app_nil_end : list v62.
 
-Lemma app_ass : (l,m,n : list)(app (app l m) n)=(app l (app m n)).
+(*************************)
+(** Concatenation        *)
+(*************************)
+
+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.
+
+Lemma app_nil_end : forall l:list, l = l ++ nil.
 Proof. 
-	Intros l m n ; Elim l ; Simpl ; Auto with list.
-	Induction 1; Auto with list.
+	induction l; simpl in |- *; auto.
+        rewrite <- IHl; auto.
 Qed.
-Hints Resolve app_ass : list v62.
+Hint Resolve app_nil_end.
+
+Ltac now_show c := change c in |- *.
 
-Lemma ass_app : (l,m,n : list)(app l (app m n))=(app (app l m) n).
+Lemma app_ass : forall l m n:list, (l ++ m) ++ n = l ++ m ++ n.
 Proof. 
-	Auto with list.
+	intros. induction l; simpl in |- *; auto.
+        now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n).
+	rewrite <- IHl; auto.
 Qed.
-Hints Resolve ass_app : list v62.
+Hint Resolve app_ass.
 
-Definition tail := 
-    [l:list] <list>Cases l of  (cons _ m) => m | _ => nil end : list->list.
-                   
+Lemma ass_app : forall l m n:list, l ++ m ++ n = (l ++ m) ++ n.
+Proof. 
+	auto.
+Qed.
+Hint Resolve ass_app.
 
-Lemma nil_cons : (a:A)(m:list)~nil=(cons a m).
-  Intros; Discriminate.
+Lemma app_comm_cons : forall (x y:list) (a:A), a :: x ++ y = (a :: x) ++ y.
+Proof.
+ auto.
 Qed.
 
+Lemma app_eq_nil : forall x y:list, x ++ y = nil -> x = nil /\ y = nil.
+Proof.
+  destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
+   simpl in |- *; auto.
+  intros H; discriminate H.
+  intros; discriminate H.
+Qed.
+
+Lemma app_cons_not_nil : forall (x y:list) (a:A), nil <> x ++ a :: y.
+Proof.
+unfold not in |- *.
+  destruct x as [| a l]; simpl in |- *; intros.
+  discriminate H.
+  discriminate H.
+Qed.
+
+Lemma app_eq_unit :
+ forall (x y:list) (a:A),
+   x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil.
+
+Proof.
+  destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
+   simpl in |- *.
+  intros a H; discriminate H.
+  left; split; auto.
+  right; split; auto.
+  generalize H.
+  generalize (app_nil_end l); intros E.
+  rewrite <- E; auto.
+  intros.
+  injection H.
+  intro.
+  cut (nil = l ++ a0 :: l0); auto.
+  intro.
+  generalize (app_cons_not_nil _ _ _ H1); intro.
+  elim H2.
+Qed.
+
+Lemma app_inj_tail :
+ forall (x y:list) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b.
+Proof.
+  induction x as [| x l IHl];
+   [ destruct y as [| a l] | destruct y as [| a l0] ]; 
+   simpl in |- *; auto.
+  intros a b H.
+  injection H.
+  auto.
+  intros a0 b H.
+  injection H; intros.
+  generalize (app_cons_not_nil _ _ _ H0); destruct 1.
+  intros a b H.
+  injection H; intros.
+  cut (nil = l ++ a :: nil); auto.
+  intro.
+  generalize (app_cons_not_nil _ _ _ H2); destruct 1.
+  intros a0 b H.
+  injection H; intros.
+  destruct (IHl l0 a0 b H0). 
+  split; auto.
+  rewrite <- H1; rewrite <- H2; reflexivity.
+Qed.
+
+(*************************)
+(** Head and tail        *)
+(*************************)
+
+Definition head (l:list) :=
+  match l with
+  | nil => error
+  | x :: _ => value x
+  end.
+
+Definition tail (l:list) : list :=
+  match l with
+  | nil => nil
+  | a :: m => m
+  end.
+
 (****************************************)
-(* Length of lists                      *)
+(** Length of lists                     *)
 (****************************************)
 
-Fixpoint length [l:list] : nat 
-   := <nat>Cases l of (cons _ m) => (S (length m)) | _ => O end.
+Fixpoint length (l:list) : nat :=
+  match l with
+  | nil => 0
+  | _ :: m => S (length m)
+  end.
 
 (******************************)
-(* Length order of lists      *)
+(** Length order of lists     *)
 (******************************)
 
 Section length_order.
-Definition lel := [l,m:list](le (length l) (length m)).
+Definition lel (l m:list) := length l <= length m.
 
-Hints Unfold lel : list.
+Variables a b : A.
+Variables l m n : list.
 
-Variables a,b:A.
-Variables l,m,n:list.
-
-Lemma lel_refl : (lel l l).
+Lemma lel_refl : lel l l.
 Proof. 
-	Unfold lel ; Auto with list.
+	unfold lel in |- *; auto with arith.
 Qed.
 
-Lemma lel_trans : (lel l m)->(lel m n)->(lel l n).
+Lemma lel_trans : lel l m -> lel m n -> lel l n.
 Proof. 
-	Unfold lel ; Intros.
-        Apply le_trans with (length m) ; Auto with list.
+	unfold lel in |- *; 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 (cons a l) (cons b m)).
+Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).
 Proof. 
-	Unfold lel ; Simpl ; Auto with list arith.
+	unfold lel in |- *; simpl in |- *; auto with arith.
 Qed.
 
-Lemma lel_cons : (lel l m)->(lel l (cons b m)).
+Lemma lel_cons : lel l m -> lel l (b :: m).
 Proof. 
-	Unfold lel ; Simpl ; Auto with list arith.
+	unfold lel in |- *; simpl in |- *; auto with arith.
 Qed.
 
-Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m).
+Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m.
 Proof. 
-	Unfold lel ; Simpl ; Auto with list arith.
+	unfold lel in |- *; simpl in |- *; auto with arith.
 Qed.
 
-Lemma lel_nil : (l':list)(lel l' nil)->(nil=l').
+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 (le (S (length y)) O); Auto with list arith.
+	intro l'; elim l'; auto with arith.
+	intros a' y H H0.
+        now_show (nil = a' :: y).
+	absurd (S (length y) <= 0); auto with arith.
 Qed.
 End length_order.
 
-Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons : list v62.
+Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons.
+
+(*********************************)
+(** The [In] predicate           *)
+(*********************************)
+
+Fixpoint In (a:A) (l:list) {struct l} : Prop :=
+  match l with
+  | nil => False
+  | b :: m => b = a \/ In a m
+  end.
+
+Lemma in_eq : forall (a:A) (l:list), In a (a :: l).
+Proof. 
+	simpl in |- *; auto.
+Qed.
+Hint Resolve in_eq.
+
+Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (a :: l).
+Proof. 
+	simpl in |- *; auto.
+Qed.
+Hint Resolve in_cons.
+
+Lemma in_nil : forall a:A, ~ In a nil.
+Proof.
+  unfold not in |- *; intros a H; inversion_clear H.
+Qed.
+
+
+Lemma in_inv : forall (a b:A) (l:list), In b (a :: l) -> a = b \/ In b l.
+Proof.
+ intros a b l H; inversion_clear H; auto.
+Qed.
+
+Lemma In_dec :
+ (forall x y:A, {x = y} + {x <> y}) ->
+ forall (a:A) (l:list), {In a l} + {~ In a l}.
+
+Proof.
+  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.
+Qed.
+
+Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m.
+Proof. 
+	intros l m a.
+	elim l; simpl in |- *; auto.
+	intros a0 y H H0.
+	now_show ((a0 = a \/ In a y) \/ In a m).
+	elim H0; auto.
+	intro H1.
+        now_show ((a0 = a \/ In a y) \/ In a m).
+	elim (H H1); auto.
+Qed.
+Hint Immediate in_app_or.
+
+Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (l ++ m).
+Proof. 
+	intros l m a.
+	elim l; simpl in |- *; intro H.
+        now_show (In a m).
+	elim H; auto; intro H0.
+	now_show (In a m).
+	elim H0. (* subProof completed *)
+	intros y H0 H1.
+	now_show (H = a \/ In a (y ++ m)).
+	elim H1; auto 4.
+	intro H2.
+	now_show (H = a \/ In a (y ++ m)).
+	elim H2; auto.
+Qed.
+Hint Resolve in_or_app.
+
+(***************************)
+(** Set inclusion on list  *)
+(***************************)
 
-Fixpoint In  [a:A;l:list] : Prop :=
-      Cases l of
-         nil => False 
-      | (cons b m) => (b=a)\/(In a m)
-      end.
+Definition incl (l m:list) := forall a:A, In a l -> In a m.
+Hint Unfold incl.
 
-Lemma in_eq : (a:A)(l:list)(In a (cons a l)).
+Lemma incl_refl : forall l:list, incl l l.
 Proof. 
-	Simpl ; Auto with list.
+	auto.
 Qed.
-Hints Resolve in_eq : list v62.
+Hint Resolve incl_refl.
 
-Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)).
+Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (a :: m).
 Proof. 
-	Simpl ; Auto with list.
+	auto.
 Qed.
-Hints Resolve in_cons : list v62.
+Hint Immediate incl_tl.
 
-Lemma in_app_or : (l,m:list)(a:A)(In a (app l m))->((In a l)\/(In a m)).
+Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n.
 Proof. 
-	Intros l m a.
-	Elim l ; Simpl ; 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.
-Hints Immediate in_app_or : list v62.
-
-Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (app l m)).
+	auto.
+Qed.
+
+Lemma incl_appl : forall l m n:list, incl l n -> incl l (n ++ m).
 Proof. 
-	Intros l m a.
-	Elim l ; Simpl ; 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.
-Hints Resolve in_or_app : list v62.
-
-Definition incl := [l,m:list](a:A)(In a l)->(In a m).
-
-Hints Unfold  incl : list v62.
-
-Lemma incl_refl : (l:list)(incl l l).
+	auto.
+Qed.
+Hint Immediate incl_appl.
+
+Lemma incl_appr : forall l m n:list, incl l n -> incl l (m ++ n).
 Proof. 
-	Auto with list.
+	auto.
 Qed.
-Hints Resolve incl_refl : list v62.
+Hint Immediate incl_appr.
 
-Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)).
+Lemma incl_cons :
+ forall (a:A) (l m:list), In a m -> incl l m -> incl (a :: l) m.
 Proof. 
-	Auto with list.
+	unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
+        now_show (In a0 m).
+	elim H1.
+	now_show (a = a0 -> In a0 m).
+	elim H1; auto; intro H2.
+	now_show (a = a0 -> In a0 m).
+	elim H2; auto. (* solves subgoal *)
+	now_show (In a0 l -> In a0 m).
+	auto.
 Qed.
-Hints Immediate incl_tl : list v62.
+Hint Resolve incl_cons.
 
-Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n).
+Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (l ++ m) n.
 Proof. 
-	Auto with list.
+	unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
+        now_show (In a n).
+	elim (in_app_or _ _ _ H1); auto.
+Qed.
+Hint Resolve incl_app.
+
+(**************************)
+(** Nth element of a list *)
+(**************************)
+
+Fixpoint nth (n:nat) (l:list) (default:A) {struct l} : A :=
+  match n, l with
+  | O, x :: l' => x
+  | O, other => default
+  | S m, nil => default
+  | S m, x :: t => nth m t default
+  end.
+
+Fixpoint nth_ok (n:nat) (l:list) (default:A) {struct l} : bool :=
+  match n, l with
+  | O, x :: l' => true
+  | O, other => false
+  | S m, nil => false
+  | S m, x :: t => nth_ok m t default
+  end.
+
+Lemma nth_in_or_default :
+ forall (n:nat) (l:list) (d:A), {In (nth n l d) l} + {nth n l d = d}.
+(* Realizer nth_ok. Program_all. *)
+Proof. 
+  intros n l d; generalize n; induction l; intro n0.
+  right; case n0; trivial.
+  case n0; simpl in |- *.
+  auto.
+  intro n1; elim (IHl n1); auto.     
 Qed.
 
-Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)).
+Lemma nth_S_cons :
+ forall (n:nat) (l:list) (d a:A),
+   In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l).
 Proof. 
-	Auto with list.
+  simpl in |- *; auto.
+Qed.
+
+Fixpoint nth_error (l:list) (n:nat) {struct n} : Exc A :=
+  match n, l with
+  | O, x :: _ => value x
+  | S n, _ :: l => nth_error l n
+  | _, _ => error
+  end.
+
+Definition nth_default (default:A) (l:list) (n:nat) : A :=
+  match nth_error l n with
+  | Some x => x
+  | None => default
+  end.
+
+Lemma nth_In :
+ forall (n:nat) (l:list) (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 |- *.
+inversion 2.
+intros d ie; right; apply hn; auto with arith.
+Qed.
+
+(********************************)
+(** Decidable equality on lists *)
+(********************************)
+
+
+Lemma list_eq_dec :
+ (forall x y:A, {x = y} + {x <> y}) -> forall x y:list, {x = y} + {x <> y}.
+Proof.
+  induction x as [| a l IHl]; destruct y as [| a0 l0]; auto.
+  destruct (H a a0) as [e| e].
+  destruct (IHl l0) as [e'| e'].
+  left; rewrite e; rewrite e'; trivial.
+  right; red in |- *; intro.
+  apply e'; injection H0; trivial.
+  right; red in |- *; intro.
+  apply e; injection H0; trivial.
+Qed.
+
+(*************************)
+(**  Reverse             *)
+(*************************)
+
+Fixpoint rev (l:list) : list :=
+  match l with
+  | nil => nil
+  | x :: l' => rev l' ++ x :: nil
+  end.
+
+Lemma distr_rev : forall x y:list, rev (x ++ y) = rev y ++ rev x.
+Proof.
+ induction x as [| a l IHl].
+ destruct y as [| a l].
+ simpl in |- *.
+ auto.
+
+ simpl in |- *.
+ apply app_nil_end; auto.
+
+ intro y.
+ simpl in |- *.
+ rewrite (IHl y).
+ apply (app_ass (rev y) (rev l) (a :: nil)).
+Qed.
+
+Remark rev_unit : forall (l:list) (a:A), rev (l ++ a :: nil) = a :: rev l.
+Proof.
+ intros.
+ apply (distr_rev l (a :: nil)); simpl in |- *; auto.
+Qed.
+
+Lemma rev_involutive : forall l:list, rev (rev l) = l.
+Proof.
+ induction l as [| a l IHl].
+ simpl in |- *; auto.
+
+ simpl in |- *.
+ rewrite (rev_unit (rev l) a).
+ rewrite IHl; auto.
+Qed.
+
+(*********************************************)
+(**  Reverse Induction Principle on Lists    *)
+(*********************************************)
+
+Section Reverse_Induction.
+
+Unset Implicit Arguments.
+
+Remark rev_list_ind :
+ forall P:list -> Prop,
+   P nil ->
+   (forall (a:A) (l:list), P (rev l) -> P (rev (a :: l))) ->
+   forall l:list, P (rev l).
+Proof.
+ induction l; auto.
+Qed.
+Set Implicit Arguments.
+
+Lemma rev_ind :
+ forall P:list -> Prop,
+   P nil ->
+   (forall (x:A) (l:list), P l -> P (l ++ x :: nil)) -> forall l:list, P l.
+Proof.
+ intros.
+ generalize (rev_involutive l).
+ intros E; rewrite <- E.
+ apply (rev_list_ind P).
+ auto.
+
+ simpl in |- *.
+ intros.
+ apply (H0 a (rev l0)).
+ auto.
 Qed.
-Hints Immediate incl_appl : list v62.
 
-Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)).
+End Reverse_Induction.
+
+End Lists.
+
+Implicit Arguments nil [A].
+
+Hint Resolve nil_cons app_nil_end ass_app app_ass: 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 lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
+  datatypes v62.
+Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62.
+Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
+  incl_app: datatypes v62.
+
+Section Functions_on_lists.
+
+(****************************************************************)
+(** Some generic functions on lists and basic functions of them *)
+(****************************************************************)
+
+Section Map.
+Variables A B : Set.
+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.
+End Map.
+
+Lemma in_map :
+ forall (A B:Set) (f:A -> B) (l:list A) (x:A), In x l -> In (f x) (map f l).
 Proof. 
-	Auto with list.
+  induction l as [| a l IHl]; simpl in |- *;
+   [ auto
+   | destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ].
 Qed.
-Hints Immediate incl_appr : list v62.
 
-Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m).
+Fixpoint flat_map (A B:Set) (f:A -> list B) (l:list A) {struct l} : 
+ list B :=
+  match l with
+  | nil => nil
+  | cons x t => app (f x) (flat_map f t)
+  end.
+
+Fixpoint list_prod (A B:Set) (l:list A) (l':list B) {struct l} :
+ list (A * B) :=
+  match l with
+  | nil => nil
+  | cons x t => app (map (fun y:B => (x, y)) l') (list_prod t l')
+  end.
+
+Lemma in_prod_aux :
+ forall (A B:Set) (x:A) (y:B) (l:list B),
+   In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).
 Proof. 
-	Unfold incl ; Simpl ; 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.
-Hints Resolve incl_cons : list v62.
-
-Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (app l m) n).
+  induction l;
+   [ simpl in |- *; auto
+   | simpl in |- *; destruct 1 as [H1| ];
+      [ left; rewrite H1; trivial | right; auto ] ].
+Qed.
+
+Lemma in_prod :
+ forall (A B:Set) (l:list A) (l':list B) (x:A) (y:B),
+   In x l -> In y l' -> In (x, y) (list_prod l l').
 Proof. 
-	Unfold incl ; Simpl ; 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.
-Hints Resolve incl_app : list v62.
+  induction l;
+   [ simpl in |- *; tauto
+   | simpl in |- *; intros; apply in_or_app; destruct H;
+      [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ].
+Qed.
+
+(** [(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:Set) (l:list A) (l':list B) {struct l} :
+ list (list (A * B)) :=
+  match l with
+  | nil => cons nil nil
+  | cons x t =>
+      flat_map (fun f:list (A * B) => map (fun y:B => cons (x, y) f) l')
+        (list_power t l')
+  end.
+
+(************************************)
+(** Left-to-right iterator on lists *)
+(************************************)
+
+Section Fold_Left_Recursor.
+Variables A B : Set.
+Variable f : A -> B -> A.
+Fixpoint fold_left (l:list B) (a0:A) {struct l} : A :=
+  match l with
+  | nil => a0
+  | cons b t => fold_left t (f a0 b)
+  end.
+End Fold_Left_Recursor.
+
+(************************************)
+(** Right-to-left iterator on lists *)
+(************************************)
+
+Section Fold_Right_Recursor.
+Variables A B : Set.
+Variable f : B -> A -> A.
+Variable a0 : A.
+Fixpoint fold_right (l:list B) : A :=
+  match l with
+  | nil => a0
+  | cons b t => f b (fold_right t)
+  end.
+End Fold_Right_Recursor.
+
+Theorem fold_symmetric :
+ forall (A:Set) (f:A -> A -> A),
+   (forall x y z:A, f x (f y z) = f (f x y) z) ->
+   (forall x y:A, f x y = f y x) ->
+   forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l.
+Proof.
+destruct l as [| a l].
+reflexivity.
+simpl in |- *.
+rewrite <- H0.
+generalize a0 a.
+induction l as [| a3 l IHl]; simpl in |- *.
+trivial.
+intros.
+rewrite H.
+rewrite (H0 a2).
+rewrite <- (H a1).
+rewrite (H0 a1).
+rewrite IHl.
+reflexivity.
+Qed.
+
+End Functions_on_lists.
+
+
+(** Exporting list notations *)
+
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+
+Infix "++" := app (right associativity, at level 60) : list_scope.
+
+Open Scope list_scope.
\ No newline at end of file
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 4b7083c0a9..f2fb20f722 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -16,374 +16,383 @@
     This allow to "hide" the definitions, functions and theorems of PolyList
     and to see only the ones of ListSet *)
 
-Require PolyList.
+Require Import List.
 
 Set Implicit Arguments.
-V7only [Implicits nil [1].].
 
 Section first_definitions.
 
   Variable A : Set.
-  Hypothesis Aeq_dec : (x,y:A){x=y}+{~x=y}.
+  Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}.
 
-  Definition set := (list A).
+  Definition set := list A.
 
-  Definition empty_set := (!nil ?) : set.
+  Definition empty_set : set := nil.
 
-  Fixpoint set_add [a:A; x:set] : set :=
-    Cases x of
-    | nil => (cons a nil)
-    | (cons a1 x1) => Cases (Aeq_dec a a1) of 
-                    | (left _) => (cons a1 x1) 
-                    | (right _) => (cons a1 (set_add a x1))
-                   end
+  Fixpoint set_add (a:A) (x:set) {struct x} : set :=
+    match x with
+    | nil => a :: nil
+    | a1 :: x1 =>
+        match Aeq_dec a a1 with
+        | left _ => a1 :: x1
+        | right _ => a1 :: set_add a x1
+        end
     end.
 
 
-  Fixpoint set_mem [a:A; x:set] : bool :=
-    Cases x of
+  Fixpoint set_mem (a:A) (x:set) {struct x} : bool :=
+    match x with
     | nil => false
-    | (cons a1 x1) => Cases (Aeq_dec a a1) of 
-                    | (left _) => true 
-                    | (right _) => (set_mem a x1)
-                   end
+    | a1 :: x1 =>
+        match Aeq_dec a a1 with
+        | left _ => true
+        | 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] : set :=
-    Cases x of
+  Fixpoint set_remove (a:A) (x:set) {struct x} : set :=
+    match x with
     | nil => empty_set
-    | (cons a1 x1) => Cases (Aeq_dec a a1) of 
-                    | (left _) => x1 
-                    | (right _) => (cons a1 (set_remove a x1))
-                   end
+    | a1 :: x1 =>
+        match Aeq_dec a a1 with
+        | left _ => x1
+        | right _ => a1 :: set_remove a x1
+        end
     end.
 
-  Fixpoint set_inter [x:set] : set -> set :=
-    Cases x of
-    | nil => [y]nil
-    | (cons a1 x1) => [y]if (set_mem a1 y) 
-                      then (cons a1 (set_inter x1 y))
-		      else (set_inter x1 y)
+  Fixpoint set_inter (x:set) : set -> set :=
+    match x with
+    | nil => fun y => nil
+    | a1 :: x1 =>
+        fun y =>
+          if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y
     end.
 
-  Fixpoint set_union [x,y:set] : set :=
-    Cases y of
+  Fixpoint set_union (x y:set) {struct y} : set :=
+    match y with
     | nil => x
-    | (cons a1 y1) => (set_add a1 (set_union x y1))
+    | 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:set] : set -> set :=
-    [y]Cases x of
+  Fixpoint set_diff (x y:set) {struct x} : set :=
+    match x with
     | nil => nil
-    | (cons a1 x1) => if (set_mem a1 y) 
-                      then (set_diff x1 y)
-		      else (set_add a1 (set_diff x1 y))
+    | 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 1!A).
+  Definition set_In : A -> set -> Prop := In (A:=A).
 
-  Lemma set_In_dec : (a:A; x:set){(set_In a x)}+{~(set_In a x)}.
+  Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}.
 
   Proof.
-    Unfold set_In.
+    unfold set_In in |- *.
     (*** Realizer set_mem. Program_all. ***)
-    Induction x.
-    Auto.
-    Intros a0 x0 Ha0. Case (Aeq_dec a a0); Intro eq.
-    Rewrite eq; Simpl; Auto with datatypes.
-    Elim Ha0.
-    Auto with datatypes.
-    Right; Simpl; Unfold not; Intros [Hc1 | Hc2 ]; Auto with datatypes.
+    simple induction x.
+    auto.
+    intros a0 x0 Ha0. case (Aeq_dec a a0); intro eq.
+    rewrite eq; simpl in |- *; auto with datatypes.
+    elim Ha0.
+    auto with datatypes.
+    right; simpl in |- *; unfold not in |- *; intros [Hc1| Hc2];
+     auto with datatypes.
   Qed.
 
-  Lemma set_mem_ind : 
-    (B:Set)(P:B->Prop)(y,z:B)(a:A)(x:set)
-      ((set_In a x) -> (P y))
-       ->(P z)
-       ->(P (if (set_mem a x) then y else z)).
+  Lemma set_mem_ind :
+   forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set),
+     (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).
 
   Proof.
-    Induction x; Simpl; Intros.
-    Assumption.
-    Elim (Aeq_dec a a0); Auto with datatypes.
+    simple induction x; simpl in |- *; intros.
+    assumption.
+    elim (Aeq_dec a a0); auto with datatypes.
   Qed.
 
-  Lemma set_mem_ind2 : 
-    (B:Set)(P:B->Prop)(y,z:B)(a:A)(x:set)
-      ((set_In a x) -> (P y))
-       ->(~(set_In a x) -> (P z))
-       ->(P (if (set_mem a x) then y else z)).
+  Lemma set_mem_ind2 :
+   forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set),
+     (set_In a x -> P y) ->
+     (~ set_In a x -> P z) -> P (if set_mem a x then y else z).
 
   Proof.
-    Induction x; Simpl; Intros.
-    Apply H0; Red; Trivial.
-    Case (Aeq_dec a a0); Auto with datatypes.
-    Intro; Apply H; Intros; Auto.
-    Apply H1; Red; Intro.
-    Case H3; Auto.
+    simple induction x; simpl in |- *; intros.
+    apply H0; red in |- *; trivial.
+    case (Aeq_dec a a0); auto with datatypes.
+    intro; apply H; intros; auto.
+    apply H1; red in |- *; intro.
+    case H3; auto.
   Qed.
 
  
   Lemma set_mem_correct1 :
-    (a:A)(x:set)(set_mem a x)=true -> (set_In a x).
+   forall (a:A) (x:set), set_mem a x = true -> set_In a x.
   Proof.
-    Induction x; Simpl.
-    Discriminate.
-    Intros a0 l; Elim (Aeq_dec a a0); Auto with datatypes.
+    simple induction x; simpl in |- *.
+    discriminate.
+    intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
   Qed.
 
   Lemma set_mem_correct2 :
-    (a:A)(x:set)(set_In a x) -> (set_mem a x)=true.
+   forall (a:A) (x:set), set_In a x -> set_mem a x = true.
   Proof.
-    Induction x; Simpl.
-    Intro Ha; Elim Ha.
-    Intros a0 l; Elim (Aeq_dec a a0); Auto with datatypes.
-    Intros H1 H2 [H3 | H4].
-    Absurd a0=a; Auto with datatypes.
-    Auto with datatypes.
+    simple induction x; simpl in |- *.
+    intro Ha; elim Ha.
+    intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
+    intros H1 H2 [H3| H4].
+    absurd (a0 = a); auto with datatypes.
+    auto with datatypes.
   Qed.
 
   Lemma set_mem_complete1 :
-    (a:A)(x:set)(set_mem a x)=false -> ~(set_In a x).
+   forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.
   Proof.
-    Induction x; Simpl.
-    Tauto.
-    Intros a0 l; Elim (Aeq_dec a a0).
-    Intros; Discriminate H0.
-    Unfold not; Intros; Elim H1; Auto with datatypes.
+    simple induction x; simpl in |- *.
+    tauto.
+    intros a0 l; elim (Aeq_dec a a0).
+    intros; discriminate H0.
+    unfold not in |- *; intros; elim H1; auto with datatypes.
   Qed.
 
   Lemma set_mem_complete2 :
-    (a:A)(x:set)~(set_In a x) -> (set_mem a x)=false.
+   forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.
   Proof.
-    Induction x; Simpl.
-    Tauto.
-    Intros a0 l; Elim (Aeq_dec a a0).
-    Intros; Elim H0; Auto with datatypes.
-    Tauto.
+    simple induction x; simpl in |- *.
+    tauto.
+    intros a0 l; elim (Aeq_dec a a0).
+    intros; elim H0; auto with datatypes.
+    tauto.
   Qed.
 
-  Lemma set_add_intro1 : (a,b:A)(x:set) 
-    (set_In a x) -> (set_In a (set_add b x)).
+  Lemma set_add_intro1 :
+   forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).
 
   Proof.
-    Unfold set_In; Induction x; Simpl.
-    Auto with datatypes.
-    Intros a0 l H [ Ha0a | Hal ].
-    Elim (Aeq_dec b a0); Left; Assumption.
-    Elim (Aeq_dec b a0); Right; [ Assumption | Auto with datatypes ].
+    unfold set_In in |- *; simple induction x; simpl in |- *.
+    auto with datatypes.
+    intros a0 l H [Ha0a| Hal].
+    elim (Aeq_dec b a0); left; assumption.
+    elim (Aeq_dec b a0); right; [ assumption | auto with datatypes ].
   Qed.
 
-  Lemma set_add_intro2 : (a,b:A)(x:set) 
-    a=b -> (set_In a (set_add b x)).
+  Lemma set_add_intro2 :
+   forall (a b:A) (x:set), a = b -> set_In a (set_add b x).
 
   Proof.
-    Unfold set_In; Induction x; Simpl.
-    Auto with datatypes.
-    Intros a0 l H Hab.
-    Elim (Aeq_dec b a0); 
-    [ Rewrite Hab; Intro Hba0; Rewrite Hba0; Simpl; Auto with datatypes
-    | Auto with datatypes ].
+    unfold set_In in |- *; simple induction x; simpl in |- *.
+    auto with datatypes.
+    intros a0 l H Hab.
+    elim (Aeq_dec b a0);
+     [ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *;
+        auto with datatypes
+     | auto with datatypes ].
   Qed.
 
-  Hints Resolve set_add_intro1 set_add_intro2.
+  Hint Resolve set_add_intro1 set_add_intro2.
 
-  Lemma set_add_intro : (a,b:A)(x:set) 
-    a=b\/(set_In a x) -> (set_In a (set_add b x)).
+  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.
+    intros a b x [H1| H2]; auto with datatypes.
   Qed.
  
-  Lemma set_add_elim : (a,b:A)(x:set) 
-    (set_In a (set_add b x)) -> a=b\/(set_In a x).
+  Lemma set_add_elim :
+   forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.
 
   Proof.
-    Unfold set_In.
-    Induction x.
-    Simpl; Intros [H1|H2]; Auto with datatypes.
-    Simpl; Do 3 Intro.
-    Elim (Aeq_dec b a0).
-    Simpl; Tauto.
-    Simpl; Intros; Elim H0.
-    Trivial with datatypes.
-    Tauto.
-    Tauto.
+    unfold set_In in |- *.
+    simple induction x.
+    simpl in |- *; intros [H1| H2]; auto with datatypes.
+    simpl in |- *; do 3 intro.
+    elim (Aeq_dec b a0).
+    simpl in |- *; tauto.
+    simpl in |- *; intros; elim H0.
+    trivial with datatypes.
+    tauto.
+    tauto.
   Qed.
 
-  Lemma set_add_elim2 :  (a,b:A)(x:set) 
-    (set_In a (set_add b x)) -> ~(a=b) -> (set_In a x).
-   Intros a b x H; Case (set_add_elim H); Intros; Trivial.
-   Case H1; Trivial.
+  Lemma set_add_elim2 :
+   forall (a b:A) (x:set), set_In a (set_add b x) -> a <> b -> set_In a x.
+   intros a b x H; case (set_add_elim _ _ _ H); intros; trivial.
+   case H1; trivial.
    Qed.
 
-  Hints Resolve set_add_intro set_add_elim set_add_elim2.
+  Hint Resolve set_add_intro set_add_elim set_add_elim2.
 
-  Lemma set_add_not_empty : (a:A)(x:set)~(set_add a x)=empty_set.
+  Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.
   Proof.
-    Induction x; Simpl.
-    Discriminate.
-    Intros; Elim  (Aeq_dec a a0); Intros; Discriminate.
+    simple induction x; simpl in |- *.
+    discriminate.
+    intros; elim (Aeq_dec a a0); intros; discriminate.
   Qed.   
 
 
-  Lemma set_union_intro1 : (a:A)(x,y:set)
-    (set_In a x) -> (set_In a (set_union x y)).
+  Lemma set_union_intro1 :
+   forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).
   Proof.
-    Induction y; Simpl; Auto with datatypes.
+    simple induction y; simpl in |- *; auto with datatypes.
   Qed.
 
-  Lemma set_union_intro2 : (a:A)(x,y:set)
-    (set_In a y) -> (set_In a (set_union x y)).
+  Lemma set_union_intro2 :
+   forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).
   Proof.
-    Induction y; Simpl.
-    Tauto.
-    Intros; Elim H0; Auto with datatypes.
+    simple induction y; simpl in |- *.
+    tauto.
+    intros; elim H0; auto with datatypes.
   Qed.
 
-  Hints Resolve set_union_intro2 set_union_intro1.
+  Hint Resolve set_union_intro2 set_union_intro1.
 
-  Lemma set_union_intro : (a:A)(x,y:set)
-    (set_In a x)\/(set_In a y) -> (set_In a (set_union x y)).
+  Lemma set_union_intro :
+   forall (a:A) (x y:set),
+     set_In a x \/ set_In a y -> set_In a (set_union x y).
   Proof.
-    Intros; Elim H; Auto with datatypes.
+    intros; elim H; auto with datatypes.
   Qed.
 
-  Lemma set_union_elim : (a:A)(x,y:set)
-    (set_In a (set_union x y)) -> (set_In a x)\/(set_In a y).
+  Lemma set_union_elim :
+   forall (a:A) (x y:set),
+     set_In a (set_union x y) -> set_In a x \/ set_In a y.
   Proof.
-    Induction y; Simpl.
-    Auto with datatypes.
-    Intros.
-    Generalize (set_add_elim H0).
-    Intros [H1 | H1].
-    Auto with datatypes.
-    Tauto.
+    simple induction y; simpl in |- *.
+    auto with datatypes.
+    intros.
+    generalize (set_add_elim _ _ _ H0).
+    intros [H1| H1].
+    auto with datatypes.
+    tauto.
   Qed.
 
-  Lemma set_union_emptyL : (a:A)(x:set)(set_In a (set_union empty_set x)) -> (set_In a x).
-    Intros a x H; Case (set_union_elim H); Auto Orelse Contradiction.
+  Lemma set_union_emptyL :
+   forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x.
+    intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
   Qed.
 
 
-  Lemma set_union_emptyR : (a:A)(x:set)(set_In a (set_union x empty_set)) -> (set_In a x).
-    Intros a x H; Case (set_union_elim H); Auto Orelse Contradiction.
+  Lemma set_union_emptyR :
+   forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x.
+    intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
   Qed.
 
 
-  Lemma set_inter_intro :  (a:A)(x,y:set)
-    (set_In a x) -> (set_In a y) -> (set_In a (set_inter x y)).
+  Lemma set_inter_intro :
+   forall (a:A) (x y:set),
+     set_In a x -> set_In a y -> set_In a (set_inter x y).
   Proof.
-    Induction x.
-    Auto with datatypes.
-    Simpl; Intros a0 l Hrec y [Ha0a | Hal] Hy.
-    Simpl; Rewrite Ha0a.
-    Generalize (!set_mem_correct1 a y).
-    Generalize (!set_mem_complete1 a y).
-    Elim (set_mem a y); Simpl; Intros.
-    Auto with datatypes.
-    Absurd (set_In a y); Auto with datatypes.
-    Elim (set_mem a0 y); [ Right; Auto with datatypes | Auto with datatypes].     
+    simple induction x.
+    auto with datatypes.
+    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy.
+    simpl in |- *; rewrite Ha0a.
+    generalize (set_mem_correct1 a y).
+    generalize (set_mem_complete1 a y).
+    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 ].     
   Qed.
 
-  Lemma set_inter_elim1 : (a:A)(x,y:set)
-    (set_In a (set_inter x y)) -> (set_In a x).
+  Lemma set_inter_elim1 :
+   forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a x.
   Proof.
-    Induction x.
-    Auto with datatypes.
-    Simpl; Intros a0 l Hrec y.
-    Generalize (!set_mem_correct1 a0 y).
-    Elim (set_mem a0 y); Simpl; Intros.
-    Elim H0; EAuto with datatypes.
-    EAuto with datatypes.
+    simple induction x.
+    auto with datatypes.
+    simpl in |- *; intros a0 l Hrec y.
+    generalize (set_mem_correct1 a0 y).
+    elim (set_mem a0 y); simpl in |- *; intros.
+    elim H0; eauto with datatypes.
+    eauto with datatypes.
   Qed.
 
-  Lemma set_inter_elim2 : (a:A)(x,y:set)
-    (set_In a (set_inter x y)) -> (set_In a y).
+  Lemma set_inter_elim2 :
+   forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.
   Proof.
-    Induction x.
-    Simpl; Tauto.
-    Simpl; Intros a0 l Hrec y.
-    Generalize (!set_mem_correct1 a0 y).
-    Elim (set_mem a0 y); Simpl; Intros.
-    Elim H0; [ Intro Hr; Rewrite <- Hr; EAuto with datatypes  | EAuto with datatypes ] .
-    EAuto with datatypes.
+    simple induction x.
+    simpl in |- *; tauto.
+    simpl in |- *; intros a0 l Hrec y.
+    generalize (set_mem_correct1 a0 y).
+    elim (set_mem a0 y); simpl in |- *; intros.
+    elim H0;
+     [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ].
+    eauto with datatypes.
   Qed.
 
-  Hints Resolve set_inter_elim1 set_inter_elim2.
+  Hint Resolve set_inter_elim1 set_inter_elim2.
 
-  Lemma set_inter_elim : (a:A)(x,y:set)
-    (set_In a (set_inter x y)) -> (set_In a x)/\(set_In a y).
+  Lemma set_inter_elim :
+   forall (a:A) (x y:set),
+     set_In a (set_inter x y) -> set_In a x /\ set_In a y.
   Proof.
-    EAuto with datatypes.
+    eauto with datatypes.
   Qed. 
 
-  Lemma set_diff_intro : (a:A)(x,y:set)
-    (set_In a x) -> ~(set_In a y) -> (set_In a (set_diff x y)).
+  Lemma set_diff_intro :
+   forall (a:A) (x y:set),
+     set_In a x -> ~ set_In a y -> set_In a (set_diff x y).
   Proof.
-    Induction x.
-    Simpl; Tauto.
-    Simpl; Intros a0 l Hrec y [Ha0a | Hal] Hay.
-    Rewrite Ha0a; Generalize (set_mem_complete2 Hay).
-    Elim (set_mem a y); [ Intro Habs; Discriminate Habs | Auto with datatypes ].
-    Elim (set_mem a0 y); Auto with datatypes.
+    simple induction x.
+    simpl in |- *; tauto.
+    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hay.
+    rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay).
+    elim (set_mem a y);
+     [ intro Habs; discriminate Habs | auto with datatypes ].
+    elim (set_mem a0 y); auto with datatypes.
   Qed.
 
-  Lemma set_diff_elim1 : (a:A)(x,y:set)
-    (set_In a (set_diff x y)) -> (set_In a x).
+  Lemma set_diff_elim1 :
+   forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.
   Proof.
-    Induction x.
-    Simpl; Tauto.
-    Simpl; Intros a0 l Hrec y; Elim (set_mem a0 y).
-    EAuto with datatypes.
-    Intro; Generalize (set_add_elim  H).
-    Intros [H1 | H2]; EAuto with datatypes.
+    simple induction x.
+    simpl in |- *; tauto.
+    simpl in |- *; intros a0 l Hrec y; elim (set_mem a0 y).
+    eauto with datatypes.
+    intro; generalize (set_add_elim _ _ _ H).
+    intros [H1| H2]; eauto with datatypes.
   Qed.
 
-  Lemma set_diff_elim2 : (a:A)(x,y:set)
-    (set_In a (set_diff x y)) -> ~(set_In a y).
-  Intros a x y; Elim x; Simpl.
-  Intros; Contradiction.
-  Intros a0 l Hrec. 
-  Apply set_mem_ind2; Auto.
-  Intros H1 H2; Case (set_add_elim H2); Intros; Auto.
-  Rewrite H; Trivial.
+  Lemma set_diff_elim2 :
+   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. 
+  apply set_mem_ind2; auto.
+  intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto.
+  rewrite H; trivial.
   Qed.
 
-  Lemma set_diff_trivial : (a:A)(x:set)~(set_In a (set_diff x x)).
-  Red; Intros a x H.
-  Apply (set_diff_elim2 H).
-  Apply (set_diff_elim1 H).
+  Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).
+  red in |- *; intros a x H.
+  apply (set_diff_elim2 _ _ _ H).
+  apply (set_diff_elim1 _ _ _ H).
   Qed.
 
-Hints Resolve set_diff_intro set_diff_trivial.
+Hint Resolve set_diff_intro set_diff_trivial.
 
 
 End first_definitions.
 
 Section other_definitions.
 
-  Variables A,B : Set.
+  Variables A B : Set.
 
-  Definition set_prod : (set A) -> (set B) -> (set A*B) := (list_prod 1!A 2!B).
+  Definition set_prod : set A -> set B -> set (A * B) :=
+    list_prod (A:=A) (B:=B).
 
   (** [B^A], set of applications from [A] to [B] *)
-  Definition set_power : (set A) -> (set B) -> (set (set A*B)) := 
-    (list_power 1!A 2!B).
+  Definition set_power : set A -> set B -> set (set (A * B)) :=
+    list_power (A:=A) (B:=B).
 
-  Definition set_map : (A->B) -> (set A) ->  (set B) := (map 1!A 2!B).
+  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 := 
-     (fold_left 1!B 2!A).
+  Definition set_fold_left : (B -> A -> B) -> set A -> B -> B :=
+    fold_left (A:=B) (B:=A).
 
-  Definition set_fold_right : (A -> B -> B) -> (set A) -> B -> B  := 
-     [f][x][b](fold_right f b x).
+  Definition set_fold_right (f:A -> B -> B) (x:set A) 
+    (b:B) : B := fold_right f b x.
 
  
 End other_definitions.
 
-V7only [Implicits nil [].].
-Unset Implicit Arguments.
+Unset Implicit Arguments.
\ No newline at end of file
diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v
index 528e61ab08..28e52a4152 100755
--- a/theories/Lists/MonoList.v
+++ b/theories/Lists/MonoList.v
@@ -10,97 +10,105 @@
 
 (** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
 
-Require Le.
+Require Import Le.
 
-Parameter List_Dom:Set.
+Parameter List_Dom : Set.
 Definition A := List_Dom.
 
-Inductive list : Set := nil : list | cons : A -> list -> list.
+Inductive list : Set :=
+  | nil : list
+  | cons : A -> list -> list.
 
-Fixpoint app [l:list] : list -> list 
-      := [m:list]<list>Cases l of
-                           nil =>  m 
-                       | (cons a l1) => (cons a (app l1 m)) 
-                   end.
+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 : (l:list)(l=(app l nil)).
+Lemma app_nil_end : forall l:list, l = app l nil.
 Proof. 
-	Intro l ; Elim l ; Simpl ; Auto.
-        Induction 1; Auto.
+	intro l; elim l; simpl in |- *; auto.
+        simple induction 1; auto.
 Qed.
-Hints Resolve app_nil_end : list v62.
+Hint Resolve app_nil_end: list v62.
 
-Lemma app_ass : (l,m,n : list)(app (app l m) n)=(app l (app m n)).
+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 ; Auto with list.
-	Induction 1; Auto with list.
+	intros l m n; elim l; simpl in |- *; auto with list.
+	simple induction 1; auto with list.
 Qed.
-Hints Resolve app_ass : list v62.
+Hint Resolve app_ass: list v62.
 
-Lemma ass_app : (l,m,n : list)(app l (app m n))=(app (app l m) n).
+Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n.
 Proof. 
-	Auto with list.
+	auto with list.
 Qed.
-Hints Resolve ass_app : list v62.
+Hint Resolve ass_app: list v62.
 
-Definition tail := 
-    [l:list] <list>Cases l of  (cons _ m) => m | _ => nil end : list->list.
+Definition tail (l:list) : list :=
+  match l return list with
+  | cons _ m => m
+  | _ => nil
+  end.
                    
 
-Lemma nil_cons : (a:A)(m:list)~nil=(cons a m).
-  Intros; Discriminate.
+Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m.
+  intros; discriminate.
 Qed.
 
 (****************************************)
 (* Length of lists                      *)
 (****************************************)
 
-Fixpoint length [l:list] : nat 
-   := <nat>Cases l of (cons _ m) => (S (length m)) | _ => O end.
+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](le (length l) (length m)).
+Definition lel (l m:list) := length l <= length m.
 
-Hints Unfold lel : list.
+Hint Unfold lel: list.
 
-Variables a,b:A.
-Variables l,m,n:list.
+Variables a b : A.
+Variables l m n : list.
 
-Lemma lel_refl : (lel l l).
+Lemma lel_refl : lel l l.
 Proof. 
-	Unfold lel ; Auto with list.
+	unfold lel in |- *; auto with list.
 Qed.
 
-Lemma lel_trans : (lel l m)->(lel m n)->(lel l n).
+Lemma lel_trans : lel l m -> lel m n -> lel l n.
 Proof. 
-	Unfold lel ; Intros.
-        Apply le_trans with (length m) ; Auto with list.
+	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)).
+Lemma lel_cons_cons : lel l m -> lel (cons a l) (cons b m).
 Proof. 
-	Unfold lel ; Simpl ; Auto with list arith.
+	unfold lel in |- *; simpl in |- *; auto with list arith.
 Qed.
 
-Lemma lel_cons : (lel l m)->(lel l (cons b m)).
+Lemma lel_cons : lel l m -> lel l (cons b m).
 Proof. 
-	Unfold lel ; Simpl ; Auto with list arith.
+	unfold lel in |- *; simpl in |- *; auto with list arith.
 Qed.
 
-Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m).
+Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m.
 Proof. 
-	Unfold lel ; Simpl ; Auto with list arith.
+	unfold lel in |- *; simpl in |- *; auto with list arith.
 Qed.
 
-Lemma lel_nil : (l':list)(lel l' nil)->(nil=l').
+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.
+	intro l'; elim l'; auto with list arith.
+	intros a' y H H0.
 	(*  <list>nil=(cons a' y)
 	    ============================
 	      H0 : (lel (cons a' y) nil)
@@ -108,35 +116,36 @@ Proof.
 	      y : list
 	      a' : A
 	      l' : list *)
-	Absurd (le (S (length y)) O); Auto with list arith.
+	absurd (S (length y) <= 0); auto with list arith.
 Qed.
 End length_order.
 
-Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons : list v62.
+Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
+  v62.
 
-Fixpoint In  [a:A;l:list] : Prop :=
-      Cases l of
-         nil => False 
-      | (cons b m) => (b=a)\/(In a m)
-      end.
+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 : (a:A)(l:list)(In a (cons a l)).
+Lemma in_eq : forall (a:A) (l:list), In a (cons a l).
 Proof. 
-	Simpl ; Auto with list.
+	simpl in |- *; auto with list.
 Qed.
-Hints Resolve in_eq : list v62.
+Hint Resolve in_eq: list v62.
 
-Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)).
+Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l).
 Proof. 
-	Simpl ; Auto with list.
+	simpl in |- *; auto with list.
 Qed.
-Hints Resolve in_cons : list v62.
+Hint Resolve in_cons: list v62.
 
-Lemma in_app_or : (l,m:list)(a:A)(In a (app l m))->((In a l)\/(In a m)).
+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 ; Auto with list.
-	Intros a0 y H H0.
+	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))
@@ -146,81 +155,82 @@ Proof.
 	      a : A
 	      m : list
 	      l : list *)
-	Elim H0 ; Auto with list.
-	Intro H1.
+	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.
+	elim (H H1); auto with list.
 Qed.
-Hints Immediate in_app_or : list v62.
+Hint Immediate in_app_or: list v62.
 
-Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (app l m)).
+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 ; Intro H.
+	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.
+	elim H; auto with list; intro H0.
 	(*  (In a m)
 	    ============================
 	      H0 : False *)
-	Elim H0. (* subProof completed *)
-	Intros y H0 H1.
+	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.
+	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.
+	elim H2; auto with list.
 Qed.
-Hints Resolve in_or_app : list v62.
+Hint Resolve in_or_app: list v62.
 
-Definition incl := [l,m:list](a:A)(In a l)->(In a m).
+Definition incl (l m:list) := forall a:A, In a l -> In a m.
 
-Hints Unfold  incl : list v62.
+Hint Unfold incl: list v62.
 
-Lemma incl_refl : (l:list)(incl l l).
+Lemma incl_refl : forall l:list, incl l l.
 Proof. 
-	Auto with list.
+	auto with list.
 Qed.
-Hints Resolve incl_refl : list v62.
+Hint Resolve incl_refl: list v62.
 
-Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)).
+Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m).
 Proof. 
-	Auto with list.
+	auto with list.
 Qed.
-Hints Immediate incl_tl : list v62.
+Hint Immediate incl_tl: list v62.
 
-Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n).
+Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n.
 Proof. 
-	Auto with list.
+	auto with list.
 Qed.
 
-Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)).
+Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m).
 Proof. 
-	Auto with list.
+	auto with list.
 Qed.
-Hints Immediate incl_appl : list v62.
+Hint Immediate incl_appl: list v62.
 
-Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)).
+Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n).
 Proof. 
-	Auto with list.
+	auto with list.
 Qed.
-Hints Immediate incl_appr : list v62.
+Hint Immediate incl_appr: list v62.
 
-Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m).
+Lemma incl_cons :
+ forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m.
 Proof. 
-	Unfold incl ; Simpl ; Intros a l m H H0 a0 H1.
+	unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
 	(*  (In a0 m)
 	    ============================
 	      H1 : (<A>a=a0)\/(In a0 l)
@@ -230,21 +240,21 @@ Proof.
 	      m : list
 	      l : list
 	      a : A *)
-	Elim H1.
+	elim H1.
 	(*  1 (<A>a=a0)->(In a0 m) *)
-	Elim H1 ; Auto with list ; Intro H2.
+	elim H1; auto with list; intro H2.
 	(*  (<A>a=a0)->(In a0 m)
 	    ============================
 	      H2 : <A>a=a0 *)
-	Elim H2 ; Auto with list. (* solves subgoal *)
+	elim H2; auto with list. (* solves subgoal *)
 	(*  2 (In a0 l)->(In a0 m) *)
-	Auto with list.
+	auto with list.
 Qed.
-Hints Resolve incl_cons : list v62.
+Hint Resolve incl_cons: list v62.
 
-Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (app l m) n).
+Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n.
 Proof. 
-	Unfold incl ; Simpl ; Intros l m n H H0 a H1.
+	unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
 	(*  (In a n)
 	    ============================
 	      H1 : (In a (app l m))
@@ -254,6 +264,6 @@ Proof.
 	      n : list
 	      m : list
 	      l : list *)
-	Elim (in_app_or l m a) ; Auto with list.
+	elim (in_app_or l m a); auto with list.
 Qed.
-Hints Resolve incl_app : list v62.
+Hint Resolve incl_app: list v62.
\ No newline at end of file
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
deleted file mode 100644
index 50b203d4e5..0000000000
--- a/theories/Lists/PolyList.v
+++ /dev/null
@@ -1,642 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-Require Le.
-
-
-Section Lists.
-
-Variable A : Set.
-
-Set Implicit Arguments.
-
-Inductive list : Set := nil : list | cons : A -> list -> list.
-
-Infix "::" cons (at level 7, right associativity) : list_scope
-  V8only (at level 60, right associativity).
-
-Open Scope list_scope.
-
-(*************************)
-(** Discrimination       *)
-(*************************)
-
-Lemma nil_cons : (a:A)(m:list)~(nil=(cons a m)).
-Proof. 
-  Intros; Discriminate.
-Qed.
-
-(*************************)
-(** Concatenation        *)
-(*************************)
-
-Fixpoint app [l:list] : list -> list 
-      := [m:list]Cases l of
-                   nil         => m 
-                 | (cons a l1) => (cons a (app l1 m))
-                 end.
-
-Infix RIGHTA 7 "^" app : list_scope
-  V8only RIGHTA 60 "++".
-
-Lemma app_nil_end : (l:list)l=(l^nil).
-Proof. 
-	NewInduction l ; Simpl ; Auto.
-        Rewrite <- IHl; Auto.
-Qed.
-Hints Resolve app_nil_end.
-
-Tactic Definition now_show c := Change c.
-V7only [Tactic Definition NowShow := now_show.].
-
-Lemma app_ass : (l,m,n : list)((l^m)^ n)=(l^(m^n)).
-Proof. 
-	Intros. NewInduction l ; Simpl ; Auto.
-        NowShow '(cons a (app (app l m) n))=(cons a (app l (app m n))).
-	Rewrite <- IHl; Auto.
-Qed.
-Hints Resolve app_ass.
-
-Lemma ass_app : (l,m,n : list)(l^(m^n))=((l^m)^n).
-Proof. 
-	Auto.
-Qed.
-Hints Resolve ass_app.
-
-Lemma app_comm_cons : (x,y:list)(a:A) (cons a (x^y))=((cons a x)^y).
-Proof.
- Auto.
-Qed.
-
-Lemma app_eq_nil: (x,y:list) (x^y)=nil -> x=nil /\ y=nil.
-Proof.
-  NewDestruct x;NewDestruct y;Simpl;Auto.
-  Intros H;Discriminate H.
-  Intros;Discriminate H.
-Qed.
-
-Lemma app_cons_not_nil: (x,y:list)(a:A)~nil=(x^(cons a y)).
-Proof.
-Unfold not .
-  NewDestruct x;Simpl;Intros.
-  Discriminate H.
-  Discriminate H.
-Qed.
-
-Lemma app_eq_unit:(x,y:list)(a:A)
-     (x^y)=(cons a nil)-> (x=nil)/\ y=(cons a nil) \/ x=(cons a nil)/\ y=nil.
-
-Proof.
-  NewDestruct x;NewDestruct y;Simpl.
-  Intros a H;Discriminate H.
-  Left;Split;Auto.
-  Right;Split;Auto.
-  Generalize H .
-  Generalize (app_nil_end  l) ;Intros E.
-  Rewrite <- E;Auto.
-  Intros.
-  Injection H.
-  Intro.
-  Cut  nil=(l^(cons a0 l0));Auto.
-  Intro.
-  Generalize (app_cons_not_nil H1); Intro.
-  Elim H2.
-Qed.
-
-Lemma app_inj_tail : (x,y:list)(a,b:A)
-   (x^(cons a nil))=(y^(cons b nil)) -> x=y /\ a=b.
-Proof.
-  NewInduction x as [|x l IHl];NewDestruct y;Simpl;Auto.
-  Intros a b H.
-  Injection H.
-  Auto.
-  Intros a0 b H.
-  Injection H;Intros.
-  Generalize (app_cons_not_nil H0) ;NewDestruct 1.
-  Intros a b H.
-  Injection H;Intros.
-  Cut   nil=(l^(cons a nil));Auto.
-  Intro.
-  Generalize (app_cons_not_nil H2) ;NewDestruct 1.
-  Intros a0 b H.
-  Injection H;Intros.
-  NewDestruct (IHl l0 a0 b H0). 
-  Split;Auto.
-  Rewrite <- H1;Rewrite <- H2;Reflexivity.
-Qed.
-
-(*************************)
-(** Head and tail        *)
-(*************************)
-
-Definition head :=
-  [l:list]Cases l of
-  | nil => Error
-  | (cons x _) => (Value x)
-  end.
-
-Definition tail : list -> list :=
-  [l:list]Cases l of
-  | nil => nil 
-  | (cons a m) => m
-  end.
-
-(****************************************)
-(** Length of lists                     *)
-(****************************************)
-
-Fixpoint length [l:list] : nat 
-   := Cases l of nil => O | (cons _ m) => (S (length m)) end.
-
-(******************************)
-(** Length order of lists     *)
-(******************************)
-
-Section length_order.
-Definition lel := [l,m:list](le (length l) (length m)).
-
-Variables a,b:A.
-Variables l,m,n:list.
-
-Lemma lel_refl : (lel l l).
-Proof. 
-	Unfold lel ; Auto with arith.
-Qed.
-
-Lemma lel_trans : (lel l m)->(lel m n)->(lel l n).
-Proof. 
-	Unfold lel ; Intros.
-        NowShow '(le (length l) (length n)).
-        Apply le_trans with (length m) ; Auto with arith.
-Qed.
-
-Lemma lel_cons_cons : (lel l m)->(lel (cons a l) (cons b m)).
-Proof. 
-	Unfold lel ; Simpl ; Auto with arith.
-Qed.
-
-Lemma lel_cons : (lel l m)->(lel l (cons b m)).
-Proof. 
-	Unfold lel ; Simpl ; Auto with arith.
-Qed.
-
-Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m).
-Proof. 
-	Unfold lel ; Simpl ; Auto with arith.
-Qed.
-
-Lemma lel_nil : (l':list)(lel l' nil)->(nil=l').
-Proof. 
-	Intro l' ; Elim l' ; Auto with arith.
-	Intros a' y H H0.
-        NowShow 'nil=(cons a' y).
-	Absurd (le (S (length y)) O); Auto with arith.
-Qed.
-End length_order.
-
-Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons.
-
-(*********************************)
-(** The [In] predicate           *)
-(*********************************)
-
-Fixpoint In  [a:A;l:list] : Prop :=
-      Cases l of nil => False | (cons b m) => (b=a)\/(In a m) end.
-
-Lemma in_eq : (a:A)(l:list)(In a (cons a l)).
-Proof. 
-	Simpl ; Auto.
-Qed.
-Hints Resolve in_eq.
-
-Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)).
-Proof. 
-	Simpl ; Auto.
-Qed.
-Hints Resolve in_cons.
-
-Lemma in_nil : (a:A)~(In a nil).
-Proof.
-  Unfold not; Intros a H; Inversion_clear H.
-Qed.
-
-
-Lemma in_inv : (a,b:A)(l:list)
-               (In b (cons a l)) -> a=b \/ (In b l).
-Proof.
- Intros a b l H ; Inversion_clear H ; Auto.
-Qed.
-
-Lemma In_dec : ((x,y:A){x=y}+{~x=y}) ->   (a:A)(l:list){(In a l)}+{~(In a l)}.
-
-Proof.
-  NewInduction l as [|a0 l IHl].
-  Right; Apply in_nil.
-  NewDestruct (H a0 a); Simpl; Auto.
-  NewDestruct IHl; Simpl; Auto. 
-  Right; Unfold not; Intros [Hc1 | Hc2]; Auto.
-Qed.
-
-Lemma in_app_or : (l,m:list)(a:A)(In a (l^m))->((In a l)\/(In a m)).
-Proof. 
-	Intros l m a.
-	Elim l ; Simpl ; Auto.
-	Intros a0 y H H0.
-	NowShow '(a0=a\/(In a y))\/(In a m).
-	Elim H0 ; Auto.
-	Intro H1.
-        NowShow '(a0=a\/(In a y))\/(In a m).
-	Elim (H H1) ; Auto.
-Qed.
-Hints Immediate in_app_or.
-
-Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (l^m)).
-Proof. 
-	Intros l m a.
-	Elim l ; Simpl ; Intro H.
-        NowShow '(In a m).
-	Elim H ; Auto ; Intro H0.
-	NowShow '(In a m).
-	Elim H0. (* subProof completed *)
-	Intros y H0 H1.
-	NowShow 'H=a\/(In a (app y m)).
-	Elim H1 ; Auto 4.
-	Intro H2.
-	NowShow 'H=a\/(In a (app y m)).
-	Elim H2 ; Auto.
-Qed.
-Hints Resolve in_or_app.
-
-(***************************)
-(** Set inclusion on list  *)
-(***************************)
-
-Definition incl := [l,m:list](a:A)(In a l)->(In a m).
-Hints Unfold  incl.
-
-Lemma incl_refl : (l:list)(incl l l).
-Proof. 
-	Auto.
-Qed.
-Hints Resolve incl_refl.
-
-Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)).
-Proof. 
-	Auto.
-Qed.
-Hints Immediate incl_tl.
-
-Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n).
-Proof. 
-	Auto.
-Qed.
-
-Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (n^m)).
-Proof. 
-	Auto.
-Qed.
-Hints Immediate incl_appl.
-
-Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (m^n)).
-Proof. 
-	Auto.
-Qed.
-Hints Immediate incl_appr.
-
-Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m).
-Proof. 
-	Unfold incl ; Simpl ; Intros a l m H H0 a0 H1.
-        NowShow '(In a0 m).
-	Elim H1.
-	NowShow 'a=a0->(In a0 m).
-	Elim H1 ; Auto ; Intro H2.
-	NowShow 'a=a0->(In a0 m).
-	Elim H2 ; Auto. (* solves subgoal *)
-	NowShow '(In a0 l)->(In a0 m).
-	Auto.
-Qed.
-Hints Resolve incl_cons.
-
-Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (l^m) n).
-Proof. 
-	Unfold incl ; Simpl ; Intros l m n H H0 a H1.
-        NowShow '(In a n).
-	Elim (in_app_or H1); Auto.
-Qed.
-Hints Resolve incl_app.
-
-(**************************)
-(** Nth element of a list *)
-(**************************)
-
-Fixpoint nth [n:nat; l:list] : A->A :=
-  [default]Cases n l of
-    O (cons x l') => x
-  | O other => default
-  | (S m) nil => default
-  | (S m) (cons x t) => (nth m t default)
-  end.
-
-Fixpoint nth_ok [n:nat; l:list] : A->bool :=
-  [default]Cases n l of
-    O (cons x l') => true
-  | O other => false
-  | (S m) nil => false
-  | (S m) (cons x t) => (nth_ok m t default)
-  end.
-
-Lemma nth_in_or_default :
-  (n:nat)(l:list)(d:A){(In (nth n l d) l)}+{(nth n l d)=d}.
-(* Realizer nth_ok. Program_all. *)
-Proof. 
-  Intros n l d; Generalize n; NewInduction l; Intro n0.
-  Right; Case n0; Trivial.
-  Case n0; Simpl.
-  Auto.
-  Intro n1; Elim (IHl n1); Auto.     
-Qed.
-
-Lemma nth_S_cons :
- (n:nat)(l:list)(d:A)(a:A)(In (nth n l d) l)
-   ->(In (nth (S n) (cons a l) d) (cons a l)).
-Proof. 
-  Simpl; Auto.
-Qed.
-
-Fixpoint nth_error [l:list;n:nat] : (Exc A) :=
-  Cases n l of
-  | O (cons x _) => (Value x)
-  | (S n) (cons _ l) => (nth_error l n)
-  | _ _ => Error 
-  end.
-
-Definition nth_default : A -> list -> nat -> A :=
-  [default,l,n]Cases (nth_error l n) of
-  | (Some x) => x
-  | None => default
-  end.
-
-Lemma nth_In :
-  (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l).
-
-Proof.
-Unfold lt; NewInduction n as [|n hn]; Simpl.
-NewDestruct l ; Simpl ;  [ Inversion 2 | Auto].
-NewDestruct l as [|a l hl] ; Simpl.
-Inversion 2.
-Intros d ie ; Right ; Apply hn ; Auto with arith.
-Qed.
-
-(********************************)
-(** Decidable equality on lists *)
-(********************************)
-
-
-Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}.
-Proof.
-  NewInduction x as [|a l IHl]; NewDestruct y as [|a0 l0]; Auto.
-  NewDestruct (H a a0) as [e|e].
-  NewDestruct (IHl l0) as [e'|e'].
-  Left; Rewrite e; Rewrite e'; Trivial.
-  Right; Red; Intro.
-  Apply e'; Injection H0; Trivial.
-  Right; Red; Intro.
-  Apply e; Injection H0; Trivial.
-Qed.
-
-(*************************)
-(**  Reverse             *)
-(*************************)
-
-Fixpoint rev [l:list] : list :=
-   Cases l of
-      nil        => nil
-   | (cons x l') => (rev l')^(cons x nil)
-   end.
-
-Lemma distr_rev : 
- (x,y:list) (rev (x^y))=((rev y)^(rev x)).
-Proof.
- NewInduction x as [|a l IHl].
- NewDestruct y.
- Simpl.
- Auto.
-
- Simpl.
- Apply app_nil_end;Auto.
-
- Intro y.
- Simpl.
- Rewrite (IHl y).
- Apply (app_ass (rev y) (rev l) (cons a nil)).
-Qed.
-
-Remark  rev_unit : (l:list)(a:A) (rev  l^(cons a nil))= (cons a (rev l)).
-Proof.
- Intros.
- Apply (distr_rev l (cons a nil));Simpl;Auto.
-Qed.
-
-Lemma idempot_rev : (l:list)(rev (rev l))=l.
-Proof.
- NewInduction l as [|a l IHl].
- Simpl;Auto.
-
- Simpl.
- Rewrite (rev_unit (rev l) a).
- Rewrite -> IHl;Auto.
-Qed.
-
-(*********************************************)
-(**  Reverse Induction Principle on Lists    *)
-(*********************************************)
-
-Section Reverse_Induction.
-
-Unset Implicit Arguments.
-
-Remark rev_list_ind: (P:list->Prop)
-      (P nil)
-       ->((a:A)(l:list)(P (rev l))->(P (rev  (cons a l)))) 
-             ->(l:list) (P (rev  l)).
-Proof.
- NewInduction l; Auto.
-Qed.
-Set Implicit Arguments.
-
-Lemma rev_ind : 
- (P:list->Prop)
-   (P nil)->
-    ((x:A)(l:list)(P l)->(P l^(cons x nil)))
-      ->(l:list)(P l).
-Proof.
- Intros.
- Generalize (idempot_rev l) .
- Intros E;Rewrite <- E.
- Apply (rev_list_ind P).
- Auto.
-
- Simpl.
- Intros.
- Apply (H0 a (rev l0)).
- Auto.
-Qed.
-
-End Reverse_Induction.
-
-End Lists.
-
-Implicits nil [1].
-
-Hints Resolve nil_cons app_nil_end ass_app app_ass : datatypes v62.
-Hints Resolve app_comm_cons  app_cons_not_nil : datatypes v62.
-Hints Immediate app_eq_nil : datatypes v62.
-Hints Resolve app_eq_unit app_inj_tail : datatypes v62. 
-Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons 
-   : datatypes v62.
-Hints Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app : datatypes v62.
-Hints Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons incl_app 
-  : datatypes v62.
-
-Section Functions_on_lists.
-
-(****************************************************************)
-(** Some generic functions on lists and basic functions of them *)
-(****************************************************************)
-
-Section Map.
-Variables A,B:Set.
-Variable  f:A->B.
-Fixpoint map [l:(list A)] : (list B) :=
-  Cases l of 
-     nil       => nil
-  | (cons a t) => (cons (f a) (map t))
-  end.
-End Map.
-
-Lemma in_map : (A,B:Set)(f:A->B)(l:(list A))(x:A)
-  (In x l) -> (In (f x) (map f l)).
-Proof. 
-  NewInduction l as [|a l IHl]; Simpl;
-  [ Auto
-  | NewDestruct 1;
-    [ Left; Apply f_equal with f:=f; Assumption
-    | Auto]
-  ].
-Qed.
-
-Fixpoint flat_map [A,B:Set; f:A->(list B); l:(list A)] : (list B) :=
-  Cases l of
-    nil => nil
-  | (cons x t) => (app (f x) (flat_map f t))
-  end.
-
-Fixpoint list_prod [A:Set; B:Set; l:(list A)] : (list B)->(list A*B) :=
-  [l']Cases l of
-    nil => nil
-  | (cons x t) => (app (map [y:B](x,y) l')
-      	       	       	     (list_prod t l'))
-  end.
-
-Lemma in_prod_aux :
-  (A:Set)(B:Set)(x:A)(y:B)(l:(list B))
-    (In y l) -> (In (x,y) (map [y0:B](x,y0) l)).
-Proof. 
-  NewInduction l;
-  [ Simpl; Auto
-  | Simpl; NewDestruct 1 as [H1|];
-    [ Left; Rewrite H1; Trivial
-    | Right; Auto]
-  ].
-Qed.
-
-Lemma in_prod : (A:Set)(B:Set)(l:(list A))(l':(list B))
-  (x:A)(y:B)(In x l)->(In y l')->(In (x,y) (list_prod l l')).
-Proof. 
-  NewInduction l;
-  [ Simpl; Tauto
-  | Simpl; Intros; Apply in_or_app; NewDestruct H;
-    [ Left; Rewrite H; Apply in_prod_aux; Assumption
-    | Right; Auto]
-  ].
-Qed.
-
-(** [(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:Set; l:(list A)] : (list B)->(list (list A*B)) :=
-  [l']Cases l of
-    nil => (cons nil nil)
-  | (cons x t) => (flat_map [f:(list A*B)](map [y:B](cons (x,y) f) l') 
-      	       	       	    (list_power t l'))
-  end.
-
-(************************************)
-(** Left-to-right iterator on lists *)
-(************************************)
-
-Section Fold_Left_Recursor.
-Variables A,B:Set.
-Variable  f:A->B->A.
-Fixpoint fold_left[l:(list B)] : A -> A :=
-[a0]Cases l of
-     nil       => a0
-  | (cons b t) => (fold_left t (f a0 b))
-  end.
-End Fold_Left_Recursor.
-
-(************************************)
-(** Right-to-left iterator on lists *)
-(************************************)
-
-Section Fold_Right_Recursor.
-Variables A,B:Set.
-Variable  f:B->A->A.
-Variable  a0:A.
-Fixpoint fold_right [l:(list B)] : A :=
-  Cases l of
-    nil => a0
-  | (cons b t) => (f b (fold_right t))
-  end.
-End Fold_Right_Recursor.
-
-Theorem fold_symmetric :
-  (A:Set)(f:A->A->A)
-   ((x,y,z:A)(f x (f y z))=(f (f x y) z))
-    ->((x,y:A)(f x y)=(f y x))
-     ->(a0:A)(l:(list A))(fold_left f l a0)=(fold_right f a0 l).
-Proof.
-NewDestruct l as [|a l].
-Reflexivity.
-Simpl.
-Rewrite <- H0.
-Generalize a0 a.
-NewInduction l as [|a3 l IHl]; Simpl.
-Trivial.
-Intros.
-Rewrite H.
-Rewrite (H0 a2).
-Rewrite <- (H a1).
-Rewrite (H0 a1).
-Rewrite IHl.
-Reflexivity.
-Qed.
-
-End Functions_on_lists.
-
-V7only [Implicits nil [].].
-
-(** Exporting list notations *)
-
-V8Infix "::" cons (at level 60, right associativity) : list_scope.
-
-Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 60 "++".
-
-Open Scope list_scope.
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v
deleted file mode 100644
index a4b6a57aae..0000000000
--- a/theories/Lists/PolyListSyntax.v
+++ /dev/null
@@ -1,10 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 9bbbe0e46c..19c564eb96 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -16,115 +16,123 @@ Section Streams.
 
 Variable A : Set.
 
-CoInductive Set Stream   := Cons : A->Stream->Stream.
+CoInductive Stream : Set :=
+    Cons : A -> Stream -> Stream.
 
 
-Definition hd  := 
-  [x:Stream] Cases x of (Cons a _) => a end.
+Definition hd (x:Stream) := match x with
+                            | Cons a _ => a
+                            end.
 
-Definition tl  := 
-  [x:Stream] Cases x of (Cons _ s) => s end.
+Definition tl (x:Stream) := match x with
+                            | Cons _ s => s
+                            end.
 
 
-Fixpoint Str_nth_tl [n:nat] : Stream->Stream := 
-  [s:Stream] Cases n of
-	          O    => s
-		|(S m) => (Str_nth_tl m (tl s))
-	    end.
+Fixpoint Str_nth_tl (n:nat) (s:Stream) {struct n} : Stream :=
+  match n with
+  | O => s
+  | S m => Str_nth_tl m (tl s)
+  end.
 
-Definition Str_nth : nat->Stream->A := [n:nat][s:Stream](hd (Str_nth_tl n s)).
+Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s).
 
 
-Lemma unfold_Stream :(x:Stream)x=(Cases x of (Cons a s) => (Cons a s) end). 
+Lemma unfold_Stream :
+ forall x:Stream, x = match x with
+                      | Cons a s => Cons a s
+                      end. 
 Proof.
-  Intro x.
-  Case x.
-  Trivial.
+  intro x.
+  case x.
+  trivial.
 Qed.
 
-Lemma tl_nth_tl : (n:nat)(s:Stream)(tl (Str_nth_tl n s))=(Str_nth_tl n (tl s)).
+Lemma tl_nth_tl :
+ forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s).
 Proof.
-  Induction n; Simpl; Auto.
+  simple induction n; simpl in |- *; auto.
 Qed.
-Hints Resolve tl_nth_tl : datatypes v62.
-
-Lemma Str_nth_tl_plus 
-: (n,m:nat)(s:Stream)(Str_nth_tl n (Str_nth_tl m s))=(Str_nth_tl (plus n m) s).
-Induction n; Simpl; Intros; Auto with datatypes.
-Rewrite <- H.
-Rewrite tl_nth_tl; Trivial with datatypes.
+Hint Resolve tl_nth_tl: datatypes v62.
+
+Lemma Str_nth_tl_plus :
+ forall (n m:nat) (s:Stream),
+   Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s.
+simple induction n; simpl in |- *; intros; auto with datatypes.
+rewrite <- H.
+rewrite tl_nth_tl; trivial with datatypes.
 Qed.
 
-Lemma Str_nth_plus 
-  : (n,m:nat)(s:Stream)(Str_nth n (Str_nth_tl m s))=(Str_nth (plus n m) s).
-Intros; Unfold Str_nth; Rewrite Str_nth_tl_plus; Trivial with datatypes.
+Lemma Str_nth_plus :
+ forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s.
+intros; unfold Str_nth in |- *; rewrite Str_nth_tl_plus;
+ trivial with datatypes.
 Qed.
 
 (** Extensional Equality between two streams  *)
 
-CoInductive EqSt  : Stream->Stream->Prop := 
-	    eqst : (s1,s2:Stream)
-		   ((hd s1)=(hd s2))->
-		   (EqSt (tl s1) (tl s2))
-                    ->(EqSt s1 s2).
+CoInductive EqSt : Stream -> Stream -> Prop :=
+    eqst :
+      forall s1 s2:Stream,
+        hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
 
 (** A coinduction principle *)
 
-Tactic Definition CoInduction proof := 
-  Cofix proof; Intros; Constructor;
-    [Clear proof | Try (Apply proof;Clear proof)].
+Ltac coinduction proof :=
+  cofix proof; intros; constructor;
+   [ clear proof | try (apply proof; clear proof) ].
 
 
 (** Extensional equality is an equivalence relation *)
 
-Theorem  EqSt_reflex : (s:Stream)(EqSt s s).
-CoInduction EqSt_reflex.
-Reflexivity.
+Theorem EqSt_reflex : forall s:Stream, EqSt s s.
+coinduction EqSt_reflex.
+reflexivity.
 Qed.
 
-Theorem sym_EqSt : 
- (s1:Stream)(s2:Stream)(EqSt s1 s2)->(EqSt s2 s1).
-(CoInduction Eq_sym).
-Case H;Intros;Symmetry;Assumption.
-Case H;Intros;Assumption.
+Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1.
+coinduction Eq_sym.
+case H; intros; symmetry  in |- *; assumption.
+case H; intros; assumption.
 Qed.
 
 
-Theorem trans_EqSt : 
- (s1,s2,s3:Stream)(EqSt s1 s2)->(EqSt s2 s3)->(EqSt s1 s3).
-(CoInduction Eq_trans).
-Transitivity (hd s2).
-Case H; Intros; Assumption.
-Case H0; Intros; Assumption.
-Apply (Eq_trans (tl s1) (tl s2) (tl s3)).
-Case H;  Trivial with datatypes.
-Case H0; Trivial with datatypes.
+Theorem trans_EqSt :
+ forall s1 s2 s3:Stream, EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3.
+coinduction Eq_trans.
+transitivity (hd s2).
+case H; intros; assumption.
+case H0; intros; assumption.
+apply (Eq_trans (tl s1) (tl s2) (tl s3)).
+case H; trivial with datatypes.
+case H0; trivial with datatypes.
 Qed.
 
 (** The definition given is equivalent to require the elements at each
     position to be equal *)
 
 Theorem eqst_ntheq :
-  (n:nat)(s1,s2:Stream)(EqSt s1 s2)->(Str_nth n s1)=(Str_nth n s2).
-Unfold Str_nth; Induction n.
-Intros s1 s2 H; Case H; Trivial with datatypes.
-Intros m hypind.
-Simpl.
-Intros s1 s2 H.
-Apply hypind.
-Case H; Trivial with datatypes.
+ forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.
+unfold Str_nth in |- *; simple induction n.
+intros s1 s2 H; case H; trivial with datatypes.
+intros m hypind.
+simpl in |- *.
+intros s1 s2 H.
+apply hypind.
+case H; trivial with datatypes.
 Qed.
 
-Theorem ntheq_eqst : 
-  (s1,s2:Stream)((n:nat)(Str_nth n s1)=(Str_nth n s2))->(EqSt s1 s2).
-(CoInduction Equiv2).
-Apply (H O).
-Intros n; Apply (H (S n)).
+Theorem ntheq_eqst :
+ forall s1 s2:Stream,
+   (forall n:nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2.
+coinduction Equiv2.
+apply (H 0).
+intros n; apply (H (S n)).
 Qed.
 
 Section Stream_Properties.
 
-Variable P : Stream->Prop.
+Variable P : Stream -> Prop.
 
 (*i
 Inductive Exists : Stream -> Prop :=
@@ -132,21 +140,21 @@ Inductive Exists : Stream -> Prop :=
   | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
 i*)
 
-Inductive   Exists :  Stream -> Prop :=
-   Here    : (x:Stream)(P x) ->(Exists x) |
-   Further : (x:Stream)(Exists (tl x))->(Exists x).
+Inductive Exists : Stream -> Prop :=
+  | Here : forall x:Stream, P x -> Exists x
+  | Further : forall x:Stream, Exists (tl x) -> Exists x.
 
-CoInductive ForAll : Stream  -> Prop :=
-    forall : (x:Stream)(P x)->(ForAll (tl x))->(ForAll x).
+CoInductive ForAll : Stream -> Prop :=
+    HereAndFurther : forall x:Stream, P x -> ForAll (tl x) -> ForAll x.
 
 
 Section Co_Induction_ForAll.
-Variable   Inv        :  Stream -> Prop.
-Hypothesis InvThenP   : (x:Stream)(Inv x)->(P x).
-Hypothesis InvIsStable: (x:Stream)(Inv x)->(Inv (tl x)).
+Variable Inv : Stream -> Prop.
+Hypothesis InvThenP : forall x:Stream, Inv x -> P x.
+Hypothesis InvIsStable : forall x:Stream, Inv x -> Inv (tl x).
 
-Theorem ForAll_coind : (x:Stream)(Inv x)->(ForAll x).
-(CoInduction ForAll_coind);Auto.
+Theorem ForAll_coind : forall x:Stream, Inv x -> ForAll x.
+coinduction ForAll_coind; auto.
 Qed.
 End Co_Induction_ForAll.
 
@@ -155,16 +163,15 @@ End Stream_Properties.
 End Streams.
 
 Section Map.
-Variables A,B : Set.
-Variable  f   : A->B.
-CoFixpoint map : (Stream A)->(Stream B) :=
- [s:(Stream A)](Cons (f (hd s)) (map (tl s))).
+Variables A B : Set.
+Variable f : A -> B.
+CoFixpoint map (s:Stream A) : Stream B := Cons (f (hd s)) (map (tl s)).
 End Map.
 
 Section Constant_Stream.
 Variable A : Set.
 Variable a : A.
-CoFixpoint const : (Stream A) := (Cons a const).
+CoFixpoint const  : Stream A := Cons a const.
 End Constant_Stream.
 
-Unset Implicit Arguments.
+Unset Implicit Arguments.
\ No newline at end of file
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index c7abe31da9..da23394c0a 100755
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -10,32 +10,32 @@
 
 (** Some programs and results about lists following CAML Manual *)
 
-Require Export PolyList.
+Require Export List.
 Set Implicit Arguments.
-Chapter Lists.
+Section Lists.
 
-Variable  A : Set.
+Variable A : Set.
 
 (**********************)
 (** The null function *)
 (**********************)
 
-Definition Isnil : (list A) -> Prop := [l:(list A)](nil A)=l.
+Definition Isnil (l:list A) : Prop := nil = l.
 
-Lemma Isnil_nil : (Isnil (nil A)).
-Red; Auto.
+Lemma Isnil_nil : Isnil nil.
+red in |- *; auto.
 Qed.
-Hints Resolve Isnil_nil.
+Hint Resolve Isnil_nil.
 
-Lemma not_Isnil_cons : (a:A)(l:(list A))~(Isnil (cons a l)).
-Unfold Isnil.
-Intros; Discriminate.
+Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l).
+unfold Isnil in |- *.
+intros; discriminate.
 Qed.
 
-Hints Resolve Isnil_nil not_Isnil_cons.
+Hint Resolve Isnil_nil not_Isnil_cons.
 
-Lemma Isnil_dec : (l:(list A)){(Isnil l)}+{~(Isnil l)}.
-Intro l; Case l;Auto.
+Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}.
+intro l; case l; auto.
 (*
 Realizer (fun l => match l with
   | nil => true
@@ -48,10 +48,11 @@ Qed.
 (** The Uncons function *)
 (************************)
 
-Lemma Uncons : (l:(list A)){a : A & { m: (list A) | (cons a m)=l}}+{Isnil l}.
-Intro l; Case l.
-Auto.
-Intros a m; Intros; Left; Exists a; Exists m; Reflexivity.
+Lemma Uncons :
+ forall l:list A, {a : A &  {m : list A | a :: m = l}} + {Isnil l}.
+intro l; case l.
+auto.
+intros a m; intros; left; exists a; exists m; reflexivity.
 (*
 Realizer (fun l => match l with
   | nil => error
@@ -64,10 +65,11 @@ Qed.
 (** The head function           *)
 (********************************)
 
-Lemma Hd : (l:(list A)){a : A | (EX m:(list A) |(cons a m)=l)}+{Isnil l}.
-Intro l; Case l.
-Auto.
-Intros a m; Intros; Left; Exists a; Exists m; Reflexivity.
+Lemma Hd :
+ forall l:list A, {a : A |  exists m : list A | a :: m = l} + {Isnil l}.
+intro l; case l.
+auto.
+intros a m; intros; left; exists a; exists m; reflexivity.
 (*
 Realizer (fun l => match l with
   | nil => error
@@ -76,11 +78,12 @@ Realizer (fun l => match l with
 *)
 Qed.
 
-Lemma Tl : (l:(list A)){m:(list A)| (EX a:A |(cons a m)=l)
-                         \/ ((Isnil l) /\ (Isnil m)) }.
-Intro l; Case l.
-Exists (nil A); Auto.
-Intros a m; Intros; Exists m; Left; Exists a; Reflexivity.
+Lemma Tl :
+ forall l:list A,
+   {m : list A | ( exists a : A | a :: m = l) \/ Isnil l /\ Isnil m}.
+intro l; case l.
+exists (nil (A:=A)); auto.
+intros a m; intros; exists m; left; exists a; reflexivity.
 (*
 Realizer (fun l => match l with
   | nil => nil
@@ -94,25 +97,25 @@ Qed.
 (****************************************)
 
 (* length is defined in List *)
-Fixpoint Length_l [l:(list A)] : nat -> nat 
-  :=  [n:nat] Cases l of
-                  nil => n
-              | (cons _ m) => (Length_l m (S n))
-	     end.
+Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat :=
+  match l with
+  | nil => n
+  | _ :: m => Length_l m (S n)
+  end.
 
 (* A tail recursive version *)
-Lemma Length_l_pf : (l:(list A))(n:nat){m:nat|(plus n (length l))=m}.
-NewInduction l as [|a m lrec].
-Intro n; Exists n; Simpl; Auto.
-Intro n; Elim (lrec (S n)); Simpl; Intros.
-Exists x; Transitivity (S (plus n (length m))); Auto.
+Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}.
+induction l as [| a m lrec].
+intro n; exists n; simpl in |- *; auto.
+intro n; elim (lrec (S n)); simpl in |- *; intros.
+exists x; transitivity (S (n + length m)); auto.
 (*
 Realizer Length_l.
 *)
 Qed.
 
-Lemma Length : (l:(list A)){m:nat|(length l)=m}.
-Intro l. Apply (Length_l_pf l O).
+Lemma Length : forall l:list A, {m : nat | length l = m}.
+intro l. apply (Length_l_pf l 0).
 (*
 Realizer (fun l -> Length_l_pf l O).
 *)
@@ -121,43 +124,42 @@ Qed.
 (*******************************)
 (** Members of lists           *)
 (*******************************)
-Inductive In_spec [a:A] : (list A) -> Prop := 
-   | in_hd : (l:(list A))(In_spec a (cons a l))
-   | in_tl : (l:(list A))(b:A)(In a l)->(In_spec a (cons b l)).
-Hints Resolve in_hd in_tl.
-Hints Unfold  In.
-Hints Resolve in_cons.
-
-Theorem In_In_spec : (a:A)(l:(list A))(In a l) <-> (In_spec a l).
-Split.
-Elim l; [ Intros; Contradiction 
-      	| Intros; Elim H0; 
-	  [ Intros; Rewrite H1; Auto
-	  | Auto ]].
-Intros; Elim H; Auto.
+Inductive In_spec (a:A) : list A -> Prop :=
+  | in_hd : forall l:list A, In_spec a (a :: l)
+  | in_tl : forall (l:list A) (b:A), In a l -> In_spec a (b :: l).
+Hint Resolve in_hd in_tl.
+Hint Unfold In.
+Hint Resolve in_cons.
+
+Theorem In_In_spec : forall (a:A) (l:list A), In a l <-> In_spec a l.
+split.
+elim l;
+ [ intros; contradiction
+ | intros; elim H0; [ intros; rewrite H1; auto | auto ] ].
+intros; elim H; auto.
 Qed.
 
-Inductive AllS [P:A->Prop] : (list A) -> Prop 
-   := allS_nil : (AllS P (nil A))
-   | allS_cons : (a:A)(l:(list A))(P a)->(AllS P l)->(AllS P (cons a l)).
-Hints Resolve allS_nil allS_cons.
+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 : (a,b:A){a=b}+{~a=b}.
+Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}.
 
-Fixpoint mem [a:A; l:(list A)] : bool :=
-  Cases l of
-    nil => false
-  | (cons b m) => if (eqA_dec a b) then [H]true else [H](mem a m)
+Fixpoint mem (a:A) (l:list A) {struct l} : bool :=
+  match l with
+  | nil => false
+  | b :: m => if eqA_dec a b then fun H => true else fun H => mem a m
   end.
 
-Hints Unfold  In.
-Lemma Mem : (a:A)(l:(list A)){(In a l)}+{(AllS [b:A]~b=a l)}.
-Intros a l.
-NewInduction l.
-Auto.
-Elim (eqA_dec a a0).
-Auto.
-Simpl. Elim IHl; Auto.
+Hint Unfold In.
+Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}.
+intros a l.
+induction l.
+auto.
+elim (eqA_dec a a0).
+auto.
+simpl in |- *. elim IHl; auto.
 (*
 Realizer mem.
 *)
@@ -167,146 +169,157 @@ Qed.
 (** Index of elements            *)
 (*********************************)
 
-Require Le.
-Require Lt.
-
-Inductive nth_spec : (list A)->nat->A->Prop :=
-  nth_spec_O : (a:A)(l:(list A))(nth_spec (cons a l) (S O) a)
-| nth_spec_S : (n:nat)(a,b:A)(l:(list A))
-           (nth_spec l n a)->(nth_spec (cons b l) (S n) a).
-Hints Resolve nth_spec_O nth_spec_S.
-
-Inductive fst_nth_spec : (list A)->nat->A->Prop :=
-  fst_nth_O : (a:A)(l:(list A))(fst_nth_spec (cons a l) (S O) a)
-| fst_nth_S : (n:nat)(a,b:A)(l:(list A))(~a=b)->
-           (fst_nth_spec l n a)->(fst_nth_spec (cons b l) (S n) a).
-Hints Resolve fst_nth_O fst_nth_S.
-
-Lemma fst_nth_nth : (l:(list A))(n:nat)(a:A)(fst_nth_spec l n a)->(nth_spec l n a).
-NewInduction 1; Auto.
+Require Import Le.
+Require Import Lt.
+
+Inductive nth_spec : list A -> nat -> A -> Prop :=
+  | nth_spec_O : forall (a:A) (l:list A), nth_spec (a :: l) 1 a
+  | nth_spec_S :
+      forall (n:nat) (a b:A) (l:list A),
+        nth_spec l n a -> nth_spec (b :: l) (S n) a.
+Hint Resolve nth_spec_O nth_spec_S.
+
+Inductive fst_nth_spec : list A -> nat -> A -> Prop :=
+  | fst_nth_O : forall (a:A) (l:list A), fst_nth_spec (a :: l) 1 a
+  | fst_nth_S :
+      forall (n:nat) (a b:A) (l:list A),
+        a <> b -> fst_nth_spec l n a -> fst_nth_spec (b :: l) (S n) a.
+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.
+induction 1; auto.
 Qed.
-Hints Immediate fst_nth_nth.
+Hint Immediate fst_nth_nth.
 
-Lemma nth_lt_O : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(lt O n).
-NewInduction 1; Auto.
+Lemma nth_lt_O : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> 0 < n.
+induction 1; auto.
 Qed.
 
-Lemma nth_le_length : (l:(list A))(n:nat)(a:A)(nth_spec l n a)->(le n (length l)).
-NewInduction 1; Simpl; Auto with arith.
+Lemma nth_le_length :
+ forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l.
+induction 1; simpl in |- *; auto with arith.
 Qed.
 
-Fixpoint Nth_func [l:(list A)] : nat -> (Exc A) 
-  := [n:nat] Cases  l  n  of 
-               (cons a _)  (S O)       => (value A a) 
-             | (cons _ l') (S (S p)) => (Nth_func l' (S p))
-             |  _ _      => Error
-            end.
-
-Lemma Nth : (l:(list A))(n:nat)
-            {a:A|(nth_spec l n a)}+{(n=O)\/(lt (length l) n)}.
-NewInduction l as [|a l IHl].
-Intro n; Case n; Simpl; Auto with arith.
-Intro n; NewDestruct n as [|[|n1]]; Simpl; Auto.
-Left; Exists a; Auto.
-NewDestruct (IHl (S n1)) as [[b]|o].
-Left; Exists b; Auto.
-Right; NewDestruct o.
-Absurd (S n1)=O; Auto.
-Auto with arith.
+Fixpoint Nth_func (l:list A) (n:nat) {struct l} : Exc A :=
+  match l, n with
+  | a :: _, S O => value a
+  | _ :: l', S (S p) => Nth_func l' (S p)
+  | _, _ => error
+  end.
+
+Lemma Nth :
+ forall (l:list A) (n:nat),
+   {a : A | nth_spec l n a} + {n = 0 \/ length l < n}.
+induction l as [| a l IHl].
+intro n; case n; simpl in |- *; auto with arith.
+intro n; destruct n as [| [| n1]]; simpl in |- *; auto.
+left; exists a; auto.
+destruct (IHl (S n1)) as [[b]| o].
+left; exists b; auto.
+right; destruct o.
+absurd (S n1 = 0); auto.
+auto with arith.
 (*
 Realizer Nth_func.
 *)
 Qed.
 
-Lemma Item : (l:(list A))(n:nat){a:A|(nth_spec l (S n) a)}+{(le (length l) n)}.
-Intros l n; Case (Nth l (S n)); Intro.
-Case s; Intro a; Left; Exists a; Auto.
-Right; Case o; Intro.
-Absurd (S n)=O; Auto.
-Auto with arith.
+Lemma Item :
+ forall (l:list A) (n:nat), {a : A | nth_spec l (S n) a} + {length l <= n}.
+intros l n; case (Nth l (S n)); intro.
+case s; intro a; left; exists a; auto.
+right; case o; intro.
+absurd (S n = 0); auto.
+auto with arith.
 Qed.
 
-Require Minus.
-Require DecBool.
-
-Fixpoint index_p [a:A;l:(list A)] : nat -> (Exc nat) := 
-   Cases l of nil => [p]Error
-     | (cons b m) => [p](ifdec (eqA_dec a b) (Value p) (index_p a m (S p)))
-   end.
-
-Lemma Index_p : (a:A)(l:(list A))(p:nat)
-     {n:nat|(fst_nth_spec l (minus (S n) p) a)}+{(AllS [b:A]~a=b l)}.
-NewInduction l as [|b m irec].
-Auto.
-Intro p.
-NewDestruct (eqA_dec a b) as [e|e].
-Left; Exists p.
-NewDestruct e; Elim minus_Sn_m; Trivial; Elim minus_n_n; Auto with arith.
-NewDestruct (irec (S p)) as [[n H]|].
-Left; Exists n; Auto with arith.
-Elim minus_Sn_m; Auto with arith.
-Apply lt_le_weak; Apply lt_O_minus_lt; Apply nth_lt_O with m a; Auto with arith.
-Auto.
+Require Import Minus.
+Require Import DecBool.
+
+Fixpoint index_p (a:A) (l:list A) {struct l} : 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))
+  end.
+
+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}.
+induction l as [| b m irec].
+auto.
+intro p.
+destruct (eqA_dec a b) as [e| e].
+left; exists p.
+destruct e; elim minus_Sn_m; trivial; elim minus_n_n; auto with arith.
+destruct (irec (S p)) as [[n H]| ].
+left; exists n; auto with arith.
+elim minus_Sn_m; auto with arith.
+apply lt_le_weak; apply lt_O_minus_lt; apply nth_lt_O with m a;
+ auto with arith.
+auto.
 Qed.
 
-Lemma Index : (a:A)(l:(list A))
-     {n:nat|(fst_nth_spec l n a)}+{(AllS [b:A]~a=b l)}.
+Lemma Index :
+ forall (a:A) (l:list A),
+   {n : nat | fst_nth_spec l n a} + {AllS (fun b:A => a <> b) l}.
 
-Intros a l; Case (Index_p a l (S O)); Auto.
-Intros (n,P); Left; Exists n; Auto.
-Rewrite (minus_n_O n); Trivial.
+intros a l; case (Index_p a l 1); auto.
+intros [n P]; left; exists n; auto.
+rewrite (minus_n_O n); trivial.
 (*
 Realizer (fun a l -> Index_p a l (S O)).
 *)
 Qed.
 
 Section Find_sec.
-Variable R,P : A -> Prop.
+Variables R P : A -> Prop.
 
-Inductive InR : (list A) -> Prop 
-   := inR_hd : (a:A)(l:(list A))(R a)->(InR (cons a l))
-   | inR_tl : (a:A)(l:(list A))(InR l)->(InR (cons a l)).
-Hints Resolve inR_hd inR_tl.
+Inductive InR : list A -> Prop :=
+  | inR_hd : forall (a:A) (l:list A), R a -> InR (a :: l)
+  | inR_tl : forall (a:A) (l:list A), InR l -> InR (a :: l).
+Hint Resolve inR_hd inR_tl.
 
-Definition InR_inv := 
-       [l:(list A)]Cases l of 
-                   nil => False 
-                | (cons b m) => (R b)\/(InR m) 
-               end.
+Definition InR_inv (l:list A) :=
+  match l with
+  | nil => False
+  | b :: m => R b \/ InR m
+  end.
 
-Lemma InR_INV : (l:(list A))(InR l)->(InR_inv l).
-NewInduction 1; Simpl; Auto.
+Lemma InR_INV : forall l:list A, InR l -> InR_inv l.
+induction 1; simpl in |- *; auto.
 Qed.
 
-Lemma InR_cons_inv : (a:A)(l:(list A))(InR (cons a l))->((R a)\/(InR l)).
-Intros a l H; Exact (InR_INV H).
+Lemma InR_cons_inv : forall (a:A) (l:list A), InR (a :: l) -> R a \/ InR l.
+intros a l H; exact (InR_INV H).
 Qed.
 
-Lemma InR_or_app : (l,m:(list A))((InR l)\/(InR m))->(InR (app l m)).
-Intros l m [|].
-NewInduction 1; Simpl; Auto.
-Intro. NewInduction l; Simpl; Auto.
+Lemma InR_or_app : forall l m:list A, InR l \/ InR m -> InR (l ++ m).
+intros l m [| ].
+induction 1; simpl in |- *; auto.
+intro. induction l; simpl in |- *; auto.
 Qed.
 
-Lemma InR_app_or : (l,m:(list A))(InR (app l m))->((InR l)\/(InR m)).
-Intros l m; Elim l; Simpl; Auto.
-Intros b l' Hrec IAc; Elim (InR_cons_inv IAc);Auto.
-Intros; Elim Hrec; Auto.
+Lemma InR_app_or : forall l m:list A, InR (l ++ m) -> InR l \/ InR m.
+intros l m; elim l; simpl in |- *; auto.
+intros b l' Hrec IAc; elim (InR_cons_inv IAc); auto.
+intros; elim Hrec; auto.
 Qed.
 
-Hypothesis RS_dec : (a:A){(R a)}+{(P a)}.
+Hypothesis RS_dec : forall a:A, {R a} + {P a}.
 
-Fixpoint find [l:(list A)] : (Exc A) := 
-	Cases l of nil => Error
-                | (cons a m) => (ifdec (RS_dec a) (Value a) (find m))
-        end.
+Fixpoint find (l:list A) : Exc A :=
+  match l with
+  | nil => error
+  | a :: m => ifdec (RS_dec a) (value a) (find m)
+  end.
 
-Lemma Find : (l:(list A)){a:A | (In a l) & (R a)}+{(AllS P l)}.
-NewInduction l as [|a m [[b H1 H2]|H]]; Auto.
-Left; Exists b; Auto.
-NewDestruct (RS_dec a).
-Left; Exists a; Auto.
-Auto.
+Lemma Find : forall l:list A, {a : A | In a l &  R a} + {AllS P l}.
+induction l as [| a m [[b H1 H2]| H]]; auto.
+left; exists b; auto.
+destruct (RS_dec a).
+left; exists a; auto.
+auto.
 (*
 Realizer find.
 *)
@@ -315,26 +328,27 @@ Qed.
 Variable B : Set.
 Variable T : A -> B -> Prop.
 
-Variable TS_dec : (a:A){c:B| (T a c)}+{(P a)}.
-
-Fixpoint try_find [l:(list A)] : (Exc B) :=
-   Cases l of
-     nil => Error
-   | (cons a l1) =>
-	   Cases (TS_dec a) of
-	     (inleft (exist c _)) => (Value c)
-	   | (inright _) => (try_find l1)
-	   end
-   end.
-
-Lemma Try_find : (l:(list A)){c:B|(EX a:A |(In a l) & (T a c))}+{(AllS P l)}.
-NewInduction l as [|a m [[b H1]|H]].
-Auto.
-Left; Exists b; NewDestruct H1 as [a' H2 H3]; Exists a'; Auto.
-NewDestruct (TS_dec a) as [[c H1]|].
-Left; Exists c.
-Exists a; Auto.
-Auto.
+Variable TS_dec : forall a:A, {c : B | T a c} + {P a}.
+
+Fixpoint try_find (l:list A) : Exc B :=
+  match l with
+  | nil => error
+  | a :: l1 =>
+      match TS_dec a with
+      | inleft (exist c _) => value c
+      | inright _ => try_find l1
+      end
+  end.
+
+Lemma Try_find :
+ forall l:list A, {c : B |  exists2 a : A | In a l & T a c} + {AllS P l}.
+induction l as [| a m [[b H1]| H]].
+auto.
+left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto.
+destruct (TS_dec a) as [[c H1]| ].
+left; exists c.
+exists a; auto.
+auto.
 (* 
 Realizer try_find.
 *)
@@ -345,17 +359,20 @@ End Find_sec.
 Section Assoc_sec.
 
 Variable B : Set.
-Fixpoint assoc [a:A;l:(list A*B)] : (Exc B) :=
-    Cases l of        nil => Error
-        | (cons (a',b) m) => (ifdec (eqA_dec a a') (Value b) (assoc a m))
-    end.
+Fixpoint assoc (a:A) (l:list (A * B)) {struct l} : 
+ Exc B :=
+  match l with
+  | nil => error
+  | (a', b) :: m => ifdec (eqA_dec a a') (value b) (assoc a m)
+  end.
 
-Inductive AllS_assoc [P:A -> Prop]: (list A*B) -> Prop := 
-      allS_assoc_nil : (AllS_assoc P (nil A*B))
-    | allS_assoc_cons : (a:A)(b:B)(l:(list A*B))
-        (P a)->(AllS_assoc P l)->(AllS_assoc P (cons (a,b) l)).
+Inductive AllS_assoc (P:A -> Prop) : list (A * B) -> Prop :=
+  | allS_assoc_nil : AllS_assoc P nil
+  | allS_assoc_cons :
+      forall (a:A) (b:B) (l:list (A * B)),
+        P a -> AllS_assoc P l -> AllS_assoc P ((a, b) :: l).
 
-Hints Resolve allS_assoc_nil allS_assoc_cons.
+Hint Resolve allS_assoc_nil allS_assoc_cons.
 
 (* The specification seems too weak: it is enough to return b if the
    list has at least an element (a,b); probably the intention is to have
@@ -364,13 +381,14 @@ Hints Resolve allS_assoc_nil allS_assoc_cons.
    (a:A)(l:(list A*B)){b:B|(In_spec (a,b) l)}+{(AllS_assoc [a':A]~(a=a') l)}.
 *)
 
-Lemma Assoc : (a:A)(l:(list A*B))(B+{(AllS_assoc [a':A]~(a=a') l)}).
-NewInduction l as [|[a' b] m assrec]. Auto.
-NewDestruct (eqA_dec a a').
-Left; Exact b.
-NewDestruct assrec as [b'|].
-Left; Exact b'.
-Right; Auto.
+Lemma Assoc :
+ forall (a:A) (l:list (A * B)), B + {AllS_assoc (fun a':A => a <> a') l}.
+induction l as [| [a' b] m assrec]. auto.
+destruct (eqA_dec a a').
+left; exact b.
+destruct assrec as [b'| ].
+left; exact b'.
+right; auto.
 (*
 Realizer assoc.
 *)
@@ -380,7 +398,6 @@ End Assoc_sec.
 
 End Lists.
 
-Hints Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons 
- : datatypes.
-Hints Immediate fst_nth_nth : datatypes.
-
+Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons:
+  datatypes.
+Hint Immediate fst_nth_nth: datatypes.