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

9 files changed, 573 insertions, 587 deletions

diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 44c2f8661..e702dbfde 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -12,45 +12,44 @@
     From : Constructing Recursion Operators in Type Theory                 
            L. Paulson  JSC (1986) 2, 325-355 *) 
 
-Require Relation_Operators.
+Require Import Relation_Operators.
 
 Section Wf_Disjoint_Union.
-Variable A,B:Set.
-Variable leA: A->A->Prop.
-Variable leB: B->B->Prop.
+Variables A B : Set.
+Variable leA : A -> A -> Prop.
+Variable leB : B -> B -> Prop.
 
 Notation Le_AsB := (le_AsB A B leA leB).
 
-Lemma acc_A_sum: (x:A)(Acc A leA x)->(Acc A+B Le_AsB (inl A B x)).
+Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
 Proof.
- NewInduction 1.
- Apply Acc_intro;Intros y H2.
- Inversion_clear H2.
- Auto with sets.
+ induction 1.
+ apply Acc_intro; intros y H2.
+ inversion_clear H2.
+ auto with sets.
 Qed.
 
-Lemma acc_B_sum: (well_founded A leA) ->(x:B)(Acc B leB x)
-                        ->(Acc A+B Le_AsB (inr A B x)).
+Lemma acc_B_sum :
+ well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
 Proof.
- NewInduction 2.
- Apply Acc_intro;Intros y H3.
- Inversion_clear H3;Auto with sets.
- Apply acc_A_sum;Auto with sets.
+ induction 2.
+ apply Acc_intro; intros y H3.
+ inversion_clear H3; auto with sets.
+ apply acc_A_sum; auto with sets.
 Qed.
 
 
-Lemma wf_disjoint_sum:
- (well_founded A leA) 
-    -> (well_founded B leB) -> (well_founded A+B Le_AsB).
+Lemma wf_disjoint_sum :
+ well_founded leA -> well_founded leB -> well_founded Le_AsB.
 Proof.
- Intros.
- Unfold well_founded .
- NewDestruct a as [a|b].
- Apply (acc_A_sum a).
- Apply (H a).
-
- Apply (acc_B_sum H b).
- Apply (H0 b).
+ intros.
+ unfold well_founded in |- *.
+ destruct a as [a| b].
+ apply (acc_A_sum a).
+ apply (H a).
+
+ apply (acc_B_sum H b).
+ apply (H0 b).
 Qed.
 
-End Wf_Disjoint_Union.
+End Wf_Disjoint_Union.
\ No newline at end of file
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index 2038b34bf..2508011dc 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -10,24 +10,23 @@
 
 (** Author: Bruno Barras *)
 
-Require Relation_Definitions.
+Require Import Relation_Definitions.
 
 Section WfInclusion.
-  Variable A:Set.
-  Variable R1,R2:A->A->Prop.
+  Variable A : Set.
+  Variables R1 R2 : A -> A -> Prop.
 
-  Lemma Acc_incl: (inclusion A R1 R2)->(z:A)(Acc A R2 z)->(Acc A R1 z).
+  Lemma Acc_incl : inclusion A R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.
   Proof.
-    NewInduction 2.
-    Apply Acc_intro;Auto with sets.
+    induction 2.
+    apply Acc_intro; auto with sets.
   Qed.
 
-  Hints Resolve Acc_incl.
+  Hint Resolve Acc_incl.
 
-  Theorem wf_incl: 
-         (inclusion A R1 R2)->(well_founded A R2)->(well_founded A R1).
+  Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
   Proof.
-    Unfold well_founded ;Auto with sets.
+    unfold well_founded in |- *; auto with sets.
   Qed.
 
-End WfInclusion.
+End WfInclusion.
\ No newline at end of file
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index ac828ac1a..66a7f5b5b 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -12,47 +12,44 @@
 
 Section Inverse_Image.
 
-  Variables A,B:Set.
-  Variable R : B->B->Prop.
-  Variable f:A->B.
+  Variables A B : Set.
+  Variable R : B -> B -> Prop.
+  Variable f : A -> B.
 
-  Local Rof : A->A->Prop := [x,y:A](R (f x) (f y)).
+  Let Rof (x y:A) : Prop := R (f x) (f y).
 
-  Remark Acc_lemma : (y:B)(Acc B R y)->(x:A)(y=(f x))->(Acc A Rof x).
-    NewInduction 1 as [y _ IHAcc]; Intros x H.
-    Apply Acc_intro; Intros y0 H1.
-    Apply (IHAcc (f y0)); Try Trivial.
-    Rewrite H; Trivial.
+  Remark Acc_lemma : forall y:B, Acc R y -> forall x:A, y = f x -> Acc Rof x.
+    induction 1 as [y _ IHAcc]; intros x H.
+    apply Acc_intro; intros y0 H1.
+    apply (IHAcc (f y0)); try trivial.
+    rewrite H; trivial.
   Qed.
 
-  Lemma Acc_inverse_image : (x:A)(Acc B R (f x)) -> (Acc A Rof x).
-    Intros; Apply (Acc_lemma (f x)); Trivial.
+  Lemma Acc_inverse_image : forall x:A, Acc R (f x) -> Acc Rof x.
+    intros; apply (Acc_lemma (f x)); trivial.
   Qed.
 
-  Theorem wf_inverse_image: (well_founded B R)->(well_founded A Rof).
-    Red; Intros; Apply Acc_inverse_image; Auto.
+  Theorem wf_inverse_image : well_founded R -> well_founded Rof.
+    red in |- *; intros; apply Acc_inverse_image; auto.
   Qed.
 
   Variable F : A -> B -> Prop.
-  Local RoF : A -> A -> Prop := [x,y]
-    (EX b : B | (F x b) & (c:B)(F y c)->(R b c)).
+  Let RoF (x y:A) : Prop :=
+     exists2 b : B | F x b & (forall c:B, F y c -> R b c).
 
-Lemma Acc_inverse_rel :
-   (b:B)(Acc B R b)->(x:A)(F x b)->(Acc A RoF x).
-NewInduction 1 as [x _ IHAcc]; Intros x0 H2.
-Constructor; Intros y H3.
-NewDestruct H3.
-Apply (IHAcc x1); Auto.
-Save.
+Lemma Acc_inverse_rel : forall b:B, Acc R b -> forall x:A, F x b -> Acc RoF x.
+induction 1 as [x _ IHAcc]; intros x0 H2.
+constructor; intros y H3.
+destruct H3.
+apply (IHAcc x1); auto.
+Qed.
 
 
-Theorem wf_inverse_rel : 
-   (well_founded B R)->(well_founded A RoF).
-    Red; Constructor; Intros.
-    Case H0; Intros.
-    Apply (Acc_inverse_rel x); Auto.
-Save.
+Theorem wf_inverse_rel : well_founded R -> well_founded RoF.
+    red in |- *; constructor; intros.
+    case H0; intros.
+    apply (Acc_inverse_rel x); auto.
+Qed.
 
 End Inverse_Image.
 
-
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 8efa124c3..e8203c399 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -13,15 +13,14 @@
     From : Constructing Recursion Operators in Type Theory                
            L. Paulson  JSC (1986) 2, 325-355  *)
 
-Require Eqdep.
-Require PolyList.
-Require PolyListSyntax.
-Require Relation_Operators.
-Require Transitive_Closure.
+Require Import Eqdep.
+Require Import List.
+Require Import Relation_Operators.
+Require Import Transitive_Closure.
 
 Section Wf_Lexicographic_Exponentiation.
-Variable A:Set.
-Variable leA: A->A->Prop.
+Variable A : Set.
+Variable leA : A -> A -> Prop.
 
 Notation Power := (Pow A leA).
 Notation Lex_Exp := (lex_exp A leA).
@@ -29,358 +28,347 @@ Notation ltl := (Ltl A leA).
 Notation Descl := (Desc A leA).
 
 Notation List := (list A).
-Notation Nil := (nil A).
+Notation Nil := (nil (A:=A)).
 (* useless but symmetric *)
-Notation Cons := (cons 1!A).
-Notation "<< x , y >>" := (exist List Descl x y) (at level 0)
-  V8only (at level 0, x,y at level 100).
-
-V7only[
-Syntax constr
-  level 1:
-    List [ (list A) ] -> ["List"]
-  | Nil  [ (nil A) ] -> ["Nil"]
-  | Cons [ (cons A) ] -> ["Cons"]
-  ;
-  level 10:
-    Cons2 [ (cons A $e $l) ] -> ["Cons " $e:L " " $l:L ].
-
-Syntax constr
-  level 1:
-  pair_sig [ (exist (list A) Desc $e $d) ] -> ["<<" $e:L "," $d:L ">>"].
-].
-Hints Resolve d_one d_nil  t_step.
-
-Lemma left_prefix : (x,y,z:List)(ltl x^y z)-> (ltl x z).
+Notation Cons := (cons (A:=A)).
+Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
+
+Hint Resolve d_one d_nil t_step.
+
+Lemma left_prefix : forall x y z:List, ltl (x ++ y) z -> ltl x z.
 Proof.
- Induction x.
- Induction z.
- Simpl;Intros H.
- Inversion_clear H. 
- Simpl;Intros;Apply (Lt_nil A leA).
- Intros a l HInd.
- Simpl.
- Intros.
- Inversion_clear H.
- Apply (Lt_hd A leA);Auto with sets.
- Apply (Lt_tl A leA).
- Apply (HInd y y0);Auto with sets.
+ simple induction x.
+ simple induction z.
+ simpl in |- *; intros H.
+ inversion_clear H. 
+ simpl in |- *; intros; apply (Lt_nil A leA).
+ intros a l HInd.
+ simpl in |- *.
+ intros.
+ inversion_clear H.
+ apply (Lt_hd A leA); auto with sets.
+ apply (Lt_tl A leA).
+ apply (HInd y y0); auto with sets.
 Qed.
 
 
-Lemma  right_prefix : 
-  (x,y,z:List)(ltl x y^z)-> (ltl x y) \/ (EX y':List | x=(y^y') /\ (ltl y' z)).
+Lemma right_prefix :
+ forall x y z:List,
+   ltl x (y ++ z) -> ltl x y \/ ( exists y' : List | x = y ++ y' /\ ltl y' z).
 Proof.
- Intros x y;Generalize x.
- Elim y;Simpl.
- Right.
- Exists x0 ;Auto with sets.
- Intros.
- Inversion H0.
- Left;Apply (Lt_nil A leA).
- Left;Apply (Lt_hd A leA);Auto with sets.
- Generalize (H x1 z H3) .
- Induction 1.
- Left;Apply (Lt_tl A leA);Auto with sets.
- Induction 1.
- Induction 1;Intros.
- Rewrite -> H8.
- Right;Exists x2 ;Auto with sets.
+ intros x y; generalize x.
+ elim y; simpl in |- *.
+ right.
+ exists x0; auto with sets.
+ intros.
+ inversion H0.
+ left; apply (Lt_nil A leA).
+ left; apply (Lt_hd A leA); auto with sets.
+ generalize (H x1 z H3).
+ simple induction 1.
+ left; apply (Lt_tl A leA); auto with sets.
+ simple induction 1.
+ simple induction 1; intros.
+ rewrite H8.
+ right; exists x2; auto with sets.
 Qed.
 
 
 
-Lemma desc_prefix: (x:List)(a:A)(Descl x^(Cons a Nil))->(Descl x).
+Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x.
 Proof.
- Intros.
- Inversion H.
- Generalize (app_cons_not_nil H1); Induction 1. 
- Cut (x^(Cons a Nil))=(Cons x0 Nil); Auto with sets.
- Intro.
- Generalize (app_eq_unit H0) .
- Induction 1; Induction 1; Intros.
- Rewrite -> H4; Auto with sets.
- Discriminate H5.
- Generalize (app_inj_tail H0) .
- Induction 1; Intros.
- Rewrite <- H4; Auto with sets.
+ intros.
+ inversion H.
+ generalize (app_cons_not_nil _ _ _ H1); simple induction 1. 
+ cut (x ++ Cons a Nil = Cons x0 Nil); auto with sets.
+ intro.
+ generalize (app_eq_unit _ _ H0).
+ simple induction 1; simple induction 1; intros.
+ rewrite H4; auto with sets.
+ discriminate H5.
+ generalize (app_inj_tail _ _ _ _ H0).
+ simple induction 1; intros.
+ rewrite <- H4; auto with sets.
 Qed.
 
-Lemma desc_tail: (x:List)(a,b:A)
-          (Descl (Cons b (x^(Cons a Nil))))-> (clos_trans A leA a b).
+Lemma desc_tail :
+ forall (x:List) (a b:A),
+   Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b.
 Proof.
- Intro.
- Apply rev_ind with  A:=A
-             P:=[x:List](a,b:A)
-          (Descl (Cons b (x^(Cons a Nil))))-> (clos_trans A leA a b).
- Intros.
-
- Inversion  H.
- Cut (Cons b (Cons a Nil))= ((Nil^(Cons b Nil))^ (Cons a Nil)); Auto with sets; Intro.
- Generalize H0.
- Intro.
- Generalize (app_inj_tail 2!(l^(Cons y Nil)) 3!(Nil^(Cons b Nil)) H4);
- Induction 1.
- Intros.
-
- Generalize (app_inj_tail H6); Induction 1; Intros.
- Generalize H1.
- Rewrite <- H10; Rewrite <- H7; Intro.
- Apply (t_step A leA); Auto with sets.
-
-
-
- Intros.
- Inversion H0.
- Generalize  (app_cons_not_nil H3); Intro.
- Elim H1.
-
- Generalize H0.
- Generalize (app_comm_cons (l^(Cons x0 Nil)) (Cons a Nil) b); Induction 1.
- Intro.
- Generalize (desc_prefix (Cons b (l^(Cons x0 Nil))) a H5); Intro.
- Generalize (H x0 b H6).
- Intro.
- Apply t_trans with A:=A  y:=x0; Auto with sets.
-
- Apply  t_step.
- Generalize H1.
- Rewrite -> H4; Intro.
-
- Generalize (app_inj_tail H8); Induction 1.
- Intros.
- Generalize H2; Generalize (app_comm_cons l (Cons x0 Nil) b).
- Intro.
- Generalize H10.
- Rewrite ->H12; Intro.
- Generalize (app_inj_tail H13); Induction 1.
- Intros.
- Rewrite <- H11; Rewrite <- H16; Auto with sets.
+ intro.
+ apply rev_ind with
+  (A := A)
+  (P := fun x:List =>
+          forall a b:A,
+            Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b).
+ intros.
+
+ inversion H.
+ cut (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil);
+  auto with sets; intro.
+ generalize H0.
+ intro.
+ generalize (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H4);
+  simple induction 1.
+ intros.
+
+ generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros.
+ generalize H1.
+ rewrite <- H10; rewrite <- H7; intro.
+ apply (t_step A leA); auto with sets.
+
+
+
+ intros.
+ inversion H0.
+ generalize (app_cons_not_nil _ _ _ H3); intro.
+ elim H1.
+
+ generalize H0.
+ generalize (app_comm_cons (l ++ Cons x0 Nil) (Cons a Nil) b);
+  simple induction 1.
+ intro.
+ generalize (desc_prefix (Cons b (l ++ Cons x0 Nil)) a H5); intro.
+ generalize (H x0 b H6).
+ intro.
+ apply t_trans with (A := A) (y := x0); auto with sets.
+
+ apply t_step.
+ generalize H1.
+ rewrite H4; intro.
+
+ generalize (app_inj_tail _ _ _ _ H8); simple induction 1.
+ intros.
+ generalize H2; generalize (app_comm_cons l (Cons x0 Nil) b).
+ intro.
+ generalize H10.
+ rewrite H12; intro.
+ generalize (app_inj_tail _ _ _ _ H13); simple induction 1.
+ intros.
+ rewrite <- H11; rewrite <- H16; auto with sets.
 Qed.
 
 
-Lemma dist_aux : (z:List)(Descl z)->(x,y:List)z=(x^y)->(Descl x)/\ (Descl y).
+Lemma dist_aux :
+ forall z:List, Descl z -> forall x y:List, z = x ++ y -> Descl x /\ Descl y.
 Proof.
- Intros z D.
- Elim D.
- Intros.
- Cut (x^y)=Nil;Auto with sets; Intro.
- Generalize (app_eq_nil H0) ; Induction 1.
- Intros.
- Rewrite -> H2;Rewrite -> H3; Split;Apply d_nil.
-
- Intros.
- Cut (x0^y)=(Cons x Nil); Auto with sets.
- Intros E.
- Generalize (app_eq_unit E); Induction 1.
- Induction 1;Intros.
- Rewrite -> H2;Rewrite -> H3; Split.
- Apply d_nil.
-
- Apply d_one.
-
- Induction 1; Intros.
- Rewrite -> H2;Rewrite -> H3; Split.
- Apply d_one.
-
- Apply d_nil.
-
- Do 5 Intro.
- Intros Hind.
- Do 2 Intro.
- Generalize x0 .
- Apply rev_ind with A:=A 
-      P:=[y0:List]
-          (x0:List)
-          ((l^(Cons y Nil))^(Cons x Nil))=(x0^y0)->(Descl x0)/\(Descl y0).
-
- Intro.
- Generalize (app_nil_end x1) ; Induction 1; Induction 1.
- Split. Apply d_conc; Auto with sets.
-
- Apply d_nil.
-
- Do 3 Intro.
- Generalize x1 .
- Apply rev_ind with 
-  A:=A 
-  P:=[l0:List]
-     (x1:A)
-      (x0:List)
-       ((l^(Cons y Nil))^(Cons x Nil))=(x0^(l0^(Cons x1 Nil)))
-         ->(Descl x0)/\(Descl (l0^(Cons x1 Nil))).
-
-
- Simpl.
- Split.
- Generalize (app_inj_tail H2) ;Induction 1.
- Induction 1;Auto with sets.
-
- Apply d_one.
- Do 5 Intro.
- Generalize (app_ass x4 (l1^(Cons x2 Nil)) (Cons x3 Nil)) .
- Induction 1.
- Generalize (app_ass x4 l1 (Cons x2 Nil)) ;Induction 1.
- Intro E.
- Generalize (app_inj_tail E) .
- Induction 1;Intros.
- Generalize (app_inj_tail H6) ;Induction 1;Intros.
- Rewrite <- H7;  Rewrite <- H10; Generalize H6.
- Generalize (app_ass x4 l1 (Cons x2 Nil)); Intro E1.
- Rewrite -> E1.
- Intro.
- Generalize (Hind x4 (l1^(Cons x2 Nil))  H11) .
- Induction 1;Split.
- Auto with sets.
-
- Generalize H14.
- Rewrite <- H10; Intro.
- Apply d_conc;Auto with sets.
+ intros z D.
+ elim D.
+ intros.
+ cut (x ++ y = Nil); auto with sets; intro.
+ generalize (app_eq_nil _ _ H0); simple induction 1.
+ intros.
+ rewrite H2; rewrite H3; split; apply d_nil.
+
+ intros.
+ cut (x0 ++ y = Cons x Nil); auto with sets.
+ intros E.
+ generalize (app_eq_unit _ _ E); simple induction 1.
+ simple induction 1; intros.
+ rewrite H2; rewrite H3; split.
+ apply d_nil.
+
+ apply d_one.
+
+ simple induction 1; intros.
+ rewrite H2; rewrite H3; split.
+ apply d_one.
+
+ apply d_nil.
+
+ do 5 intro.
+ intros Hind.
+ do 2 intro.
+ generalize x0.
+ apply rev_ind with
+  (A := A)
+  (P := fun y0:List =>
+          forall x0:List,
+            (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ y0 ->
+            Descl x0 /\ Descl y0).
+
+ intro.
+ generalize (app_nil_end x1); simple induction 1; simple induction 1.
+ split. apply d_conc; auto with sets.
+
+ apply d_nil.
+
+ do 3 intro.
+ generalize x1.
+ apply rev_ind with
+  (A := A)
+  (P := fun l0:List =>
+          forall (x1:A) (x0:List),
+            (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ l0 ++ Cons x1 Nil ->
+            Descl x0 /\ Descl (l0 ++ Cons x1 Nil)).
+
+
+ simpl in |- *.
+ split.
+ generalize (app_inj_tail _ _ _ _ H2); simple induction 1.
+ simple induction 1; auto with sets.
+
+ apply d_one.
+ do 5 intro.
+ generalize (app_ass x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil)).
+ simple induction 1.
+ generalize (app_ass x4 l1 (Cons x2 Nil)); simple induction 1.
+ intro E.
+ generalize (app_inj_tail _ _ _ _ E).
+ simple induction 1; intros.
+ generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros.
+ rewrite <- H7; rewrite <- H10; generalize H6.
+ generalize (app_ass x4 l1 (Cons x2 Nil)); intro E1.
+ rewrite E1.
+ intro.
+ generalize (Hind x4 (l1 ++ Cons x2 Nil) H11).
+ simple induction 1; split.
+ auto with sets.
+
+ generalize H14.
+ rewrite <- H10; intro.
+ apply d_conc; auto with sets.
 Qed.
 
 
 
-Lemma dist_Desc_concat : (x,y:List)(Descl x^y)->(Descl x)/\(Descl y).
+Lemma dist_Desc_concat :
+ forall x y:List, Descl (x ++ y) -> Descl x /\ Descl y.
 Proof.
-  Intros.
-  Apply (dist_aux (x^y) H x y); Auto with sets.
+  intros.
+  apply (dist_aux (x ++ y) H x y); auto with sets.
 Qed.
 
 
-Lemma desc_end:(a,b:A)(x:List) 
-   (Descl x^(Cons a Nil)) /\ (ltl x^(Cons a Nil) (Cons b Nil))
-     -> (clos_trans A leA a b). 
+Lemma desc_end :
+ forall (a b:A) (x:List),
+   Descl (x ++ Cons a Nil) /\ ltl (x ++ Cons a Nil) (Cons b Nil) ->
+   clos_trans A leA a b. 
 
 Proof.
- Intros a b x.
- Case x.
- Simpl.
- Induction 1.
- Intros.
- Inversion H1;Auto with sets.
- Inversion H3.
-
- Induction 1.
- Generalize (app_comm_cons l (Cons a Nil) a0).
- Intros E; Rewrite <- E; Intros.
- Generalize (desc_tail l a a0 H0); Intro.
- Inversion H1.
- Apply t_trans with y:=a0 ;Auto with sets.
-
- Inversion H4.
+ intros a b x.
+ case x.
+ simpl in |- *.
+ simple induction 1.
+ intros.
+ inversion H1; auto with sets.
+ inversion H3.
+
+ simple induction 1.
+ generalize (app_comm_cons l (Cons a Nil) a0).
+ intros E; rewrite <- E; intros.
+ generalize (desc_tail l a a0 H0); intro.
+ inversion H1.
+ apply t_trans with (y := a0); auto with sets.
+
+ inversion H4.
 Qed.
 
 
 
 
-Lemma  ltl_unit: (x:List)(a,b:A)
- (Descl (x^(Cons a Nil))) -> (ltl x^(Cons a Nil) (Cons b Nil))
-               -> (ltl x (Cons b Nil)).
+Lemma ltl_unit :
+ forall (x:List) (a b:A),
+   Descl (x ++ Cons a Nil) ->
+   ltl (x ++ Cons a Nil) (Cons b Nil) -> ltl x (Cons b Nil).
 Proof.
- Intro.
- Case x.
- Intros;Apply (Lt_nil A leA).
+ intro.
+ case x.
+ intros; apply (Lt_nil A leA).
 
- Simpl;Intros.
- Inversion_clear H0.
- Apply (Lt_hd A leA  a b);Auto with sets.
+ simpl in |- *; intros.
+ inversion_clear H0.
+ apply (Lt_hd A leA a b); auto with sets.
  
- Inversion_clear H1.
+ inversion_clear H1.
 Qed.
 
 
-Lemma acc_app: 
-    (x1,x2:List)(y1:(Descl x1^x2))
-     (Acc Power Lex_Exp (exist List Descl (x1^x2)  y1))
-     ->(x:List)
-        (y:(Descl x))
-         (ltl x (x1^x2))->(Acc Power Lex_Exp (exist List Descl x y)).
+Lemma acc_app :
+ forall (x1 x2:List) (y1:Descl (x1 ++ x2)),
+   Acc Lex_Exp << x1 ++ x2, y1 >> ->
+   forall (x:List) (y:Descl x), ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>.
 Proof.
- Intros.
- Apply (Acc_inv Power Lex_Exp (exist List Descl (x1^x2) y1)).
- Auto with sets.
+ intros.
+ apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)).
+ auto with sets.
 
- Unfold lex_exp ;Simpl;Auto with sets.
+ unfold lex_exp in |- *; simpl in |- *; auto with sets.
 Qed.
 
 
-Theorem wf_lex_exp :
-  (well_founded A leA)->(well_founded Power Lex_Exp).
+Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.
 Proof.
- Unfold 2 well_founded .
- Induction a;Intros x y.
- Apply Acc_intro.
- Induction y0.
- Unfold 1 lex_exp ;Simpl.
- Apply rev_ind with A:=A P:=[x:List]
-                            (x0:List)
-                             (y:(Descl x0))
-                              (ltl x0 x)
-                               ->(Acc Power Lex_Exp (exist List Descl x0 y)) .
- Intros.
- Inversion_clear H0.
-
- Intro.
- Generalize (well_founded_ind A (clos_trans A leA) (wf_clos_trans A leA H)).
- Intros GR.
- Apply GR with P:=[x0:A]
-                  (l:List)
-                   ((x1:List)
-                     (y:(Descl x1))
-                      (ltl x1 l)
-                       ->(Acc Power Lex_Exp (exist List Descl x1 y)))
-                    ->(x1:List)
-                       (y:(Descl x1))
-                        (ltl x1 (l^(Cons x0 Nil)))
-                         ->(Acc Power Lex_Exp (exist List Descl x1 y)) .
- Intro;Intros HInd; Intros.
- Generalize (right_prefix x2 l (Cons x1 Nil) H1) .
- Induction 1.
- Intro; Apply (H0 x2 y1 H3).
-
- Induction 1.
- Intro;Induction 1.
- Clear  H4  H2.
- Intro;Generalize y1 ;Clear  y1.
- Rewrite -> H2.
- Apply rev_ind with A:=A P:=[x3:List]
-                            (y1:(Descl (l^x3)))
-                             (ltl x3 (Cons x1 Nil))
-                              ->(Acc Power Lex_Exp
-                                  (exist List Descl (l^x3) y1)) .
- Intros.
- Generalize (app_nil_end l) ;Intros Heq.
- Generalize y1 .
- Clear  y1.
- Rewrite <- Heq.
- Intro.
- Apply Acc_intro.
- Induction y2.
- Unfold 1 lex_exp .
- Simpl;Intros x4 y3. Intros.
- Apply (H0 x4 y3);Auto with sets.
-
- Intros. 
- Generalize (dist_Desc_concat l (l0^(Cons x4 Nil)) y1) .
- Induction 1.
- Intros.
- Generalize (desc_end x4 x1 l0  (conj ? ? H8 H5)) ; Intros.
- Generalize y1 .
- Rewrite <- (app_ass l l0 (Cons x4 Nil)); Intro.
- Generalize (HInd x4 H9 (l^l0)) ; Intros HInd2.
- Generalize (ltl_unit l0 x4 x1 H8 H5); Intro.
- Generalize (dist_Desc_concat (l^l0) (Cons x4 Nil) y2) .
- Induction 1;Intros.
- Generalize (H4 H12 H10); Intro.
- Generalize (Acc_inv Power Lex_Exp (exist List Descl (l^l0) H12) H14) .
- Generalize (acc_app l l0 H12 H14).
- Intros f g.
- Generalize (HInd2 f);Intro.
- Apply Acc_intro.
- Induction y3.
- Unfold 1 lex_exp ;Simpl; Intros.
- Apply H15;Auto with sets.
+ unfold well_founded at 2 in |- *.
+ simple induction a; intros x y.
+ apply Acc_intro.
+ simple induction y0.
+ unfold lex_exp at 1 in |- *; simpl in |- *.
+ apply rev_ind with
+  (A := A)
+  (P := fun x:List =>
+          forall (x0:List) (y:Descl x0), ltl x0 x -> Acc Lex_Exp << x0, y >>).
+ intros.
+ inversion_clear H0.
+
+ intro.
+ generalize (well_founded_ind (wf_clos_trans A leA H)).
+ intros GR.
+ apply GR with
+  (P := fun x0:A =>
+          forall l:List,
+            (forall (x1:List) (y:Descl x1),
+               ltl x1 l -> Acc Lex_Exp << x1, y >>) ->
+            forall (x1:List) (y:Descl x1),
+              ltl x1 (l ++ Cons x0 Nil) -> Acc Lex_Exp << x1, y >>).
+ intro; intros HInd; intros.
+ generalize (right_prefix x2 l (Cons x1 Nil) H1).
+ simple induction 1.
+ intro; apply (H0 x2 y1 H3).
+
+ simple induction 1.
+ intro; simple induction 1.
+ clear H4 H2.
+ intro; generalize y1; clear y1.
+ rewrite H2.
+ apply rev_ind with
+  (A := A)
+  (P := fun x3:List =>
+          forall y1:Descl (l ++ x3),
+            ltl x3 (Cons x1 Nil) -> Acc Lex_Exp << l ++ x3, y1 >>).
+ intros.
+ generalize (app_nil_end l); intros Heq.
+ generalize y1.
+ clear y1.
+ rewrite <- Heq.
+ intro.
+ apply Acc_intro.
+ simple induction y2.
+ unfold lex_exp at 1 in |- *.
+ simpl in |- *; intros x4 y3. intros.
+ apply (H0 x4 y3); auto with sets.
+
+ intros. 
+ generalize (dist_Desc_concat l (l0 ++ Cons x4 Nil) y1).
+ simple induction 1.
+ intros.
+ generalize (desc_end x4 x1 l0 (conj H8 H5)); intros.
+ generalize y1.
+ rewrite <- (app_ass l l0 (Cons x4 Nil)); intro.
+ generalize (HInd x4 H9 (l ++ l0)); intros HInd2.
+ generalize (ltl_unit l0 x4 x1 H8 H5); intro.
+ generalize (dist_Desc_concat (l ++ l0) (Cons x4 Nil) y2).
+ simple induction 1; intros.
+ generalize (H4 H12 H10); intro.
+ generalize (Acc_inv H14).
+ generalize (acc_app l l0 H12 H14).
+ intros f g.
+ generalize (HInd2 f); intro.
+ apply Acc_intro.
+ simple induction y3.
+ unfold lex_exp at 1 in |- *; simpl in |- *; intros.
+ apply H15; auto with sets.
 Qed.
 
 
-End Wf_Lexicographic_Exponentiation.
+End Wf_Lexicographic_Exponentiation.
\ No newline at end of file
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index b8f74c9ff..d457e4190 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -10,64 +10,65 @@
 
 (** Authors: Bruno Barras, Cristina Cornes *)
 
-Require Eqdep.
-Require Relation_Operators.
-Require Transitive_Closure.
+Require Import Eqdep.
+Require Import Relation_Operators.
+Require Import Transitive_Closure.
 
 (**  From : Constructing Recursion Operators in Type Theory            
      L. Paulson  JSC (1986) 2, 325-355 *)
 
 Section WfLexicographic_Product.
-Variable A:Set.
-Variable B:A->Set.
-Variable leA: A->A->Prop.
-Variable leB: (x:A)(B x)->(B x)->Prop.
+Variable A : Set.
+Variable B : A -> Set.
+Variable leA : A -> A -> Prop.
+Variable leB : forall x:A, B x -> B x -> Prop.
 
 Notation LexProd := (lexprod A B leA leB).
 
-Hints Resolve t_step Acc_clos_trans wf_clos_trans.
+Hint Resolve t_step Acc_clos_trans wf_clos_trans.
 
-Lemma acc_A_B_lexprod : (x:A)(Acc A leA x)
-        ->((x0:A)(clos_trans A leA x0 x)->(well_founded (B x0) (leB x0)))
-                ->(y:(B x))(Acc (B x) (leB x) y)
-                        ->(Acc (sigS A B) LexProd (existS A B x y)).
+Lemma acc_A_B_lexprod :
+ forall x:A,
+   Acc leA x ->
+   (forall x0:A, clos_trans A leA x0 x -> well_founded (leB x0)) ->
+   forall y:B x, Acc (leB x) y -> Acc LexProd (existS B x y).
 Proof.
- NewInduction 1 as [x _ IHAcc]; Intros H2 y.
- NewInduction 1 as [x0 H IHAcc0];Intros.
- Apply Acc_intro.
- NewDestruct y as [x2 y1]; Intro H6.
- Simple Inversion H6; Intro.
- Cut (leA x2 x);Intros.
- Apply IHAcc;Auto with sets.
- Intros.
- Apply H2.
- Apply t_trans with x2 ;Auto with sets.
-
- Red in H2.
- Apply H2.
- Auto with sets.
-
- Injection H1.
- NewDestruct 2.
- Injection H3.
- NewDestruct 2;Auto with sets.
-
- Rewrite <- H1.
- Injection H3; Intros _ Hx1.
- Subst x1.
- Apply IHAcc0.
- Elim inj_pair2 with A B x y' x0; Assumption.
+ induction 1 as [x _ IHAcc]; intros H2 y.
+ induction 1 as [x0 H IHAcc0]; intros.
+ apply Acc_intro.
+ destruct y as [x2 y1]; intro H6.
+ simple inversion H6; intro.
+ cut (leA x2 x); intros.
+ apply IHAcc; auto with sets.
+ intros.
+ apply H2.
+ apply t_trans with x2; auto with sets.
+
+ red in H2.
+ apply H2.
+ auto with sets.
+
+ injection H1.
+ destruct 2.
+ injection H3.
+ destruct 2; auto with sets.
+
+ rewrite <- H1.
+ injection H3; intros _ Hx1.
+ subst x1.
+ apply IHAcc0.
+ elim inj_pair2 with A B x y' x0; assumption.
 Qed.
 
-Theorem wf_lexprod: 
-   (well_founded A leA) ->((x:A) (well_founded (B x) (leB x))) 
-             -> (well_founded (sigS A B) LexProd).
+Theorem wf_lexprod :
+ well_founded leA ->
+ (forall x:A, well_founded (leB x)) -> well_founded LexProd.
 Proof.
- Intros wfA wfB;Unfold well_founded .
- NewDestruct a.
- Apply acc_A_B_lexprod;Auto with sets;Intros.
- Red in wfB.
- Auto with sets.
+ intros wfA wfB; unfold well_founded in |- *.
+ destruct a.
+ apply acc_A_B_lexprod; auto with sets; intros.
+ red in wfB.
+ auto with sets.
 Qed.
 
 
@@ -75,10 +76,10 @@ End WfLexicographic_Product.
 
 
 Section Wf_Symmetric_Product.
-  Variable A:Set.
-  Variable B:Set.
-  Variable leA: A->A->Prop.
-  Variable leB: B->B->Prop.
+  Variable A : Set.
+  Variable B : Set.
+  Variable leA : A -> A -> Prop.
+  Variable leB : B -> B -> Prop.
 
   Notation Symprod := (symprod A B leA leB).
 
@@ -101,24 +102,24 @@ Proof.
 Qed.
 i*)
 
-  Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y)
-                        ->(Acc (A*B) Symprod (x,y)).
+  Lemma Acc_symprod :
+   forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod (x, y).
  Proof.
- NewInduction 1 as [x _ IHAcc]; Intros y H2.
- NewInduction H2 as [x1 H3 IHAcc1].
- Apply Acc_intro;Intros y H5.
- Inversion_clear H5;Auto with sets.
- Apply IHAcc; Auto.
- Apply Acc_intro;Trivial.
+ induction 1 as [x _ IHAcc]; intros y H2.
+ induction H2 as [x1 H3 IHAcc1].
+ apply Acc_intro; intros y H5.
+ inversion_clear H5; auto with sets.
+ apply IHAcc; auto.
+ apply Acc_intro; trivial.
 Qed.
 
 
-Lemma wf_symprod: (well_founded A leA)->(well_founded B leB)
-                        ->(well_founded (A*B) Symprod).
+Lemma wf_symprod :
+ well_founded leA -> well_founded leB -> well_founded Symprod.
 Proof.
- Red.
- NewDestruct a.
- Apply Acc_symprod;Auto with sets.
+ red in |- *.
+ destruct a.
+ apply Acc_symprod; auto with sets.
 Qed.
 
 End Wf_Symmetric_Product.
@@ -126,66 +127,66 @@ End Wf_Symmetric_Product.
 
 Section Swap.
 
-  Variable A:Set.
-  Variable R:A->A->Prop.
+  Variable A : Set.
+  Variable R : A -> A -> Prop.
 
-  Notation SwapProd :=(swapprod A R).
+  Notation SwapProd := (swapprod A R).
 
 
-  Lemma swap_Acc: (x,y:A)(Acc A*A SwapProd (x,y))->(Acc A*A SwapProd (y,x)).
+  Lemma swap_Acc : forall x y:A, Acc SwapProd (x, y) -> Acc SwapProd (y, x).
 Proof.
- Intros.
- Inversion_clear H.
- Apply Acc_intro.
- NewDestruct y0;Intros.
- Inversion_clear H;Inversion_clear H1;Apply H0.
- Apply sp_swap.
- Apply right_sym;Auto with sets.
-
- Apply sp_swap.
- Apply left_sym;Auto with sets.
-
- Apply sp_noswap.
- Apply right_sym;Auto with sets.
-
- Apply sp_noswap.
- Apply left_sym;Auto with sets.
+ intros.
+ inversion_clear H.
+ apply Acc_intro.
+ destruct y0; intros.
+ inversion_clear H; inversion_clear H1; apply H0.
+ apply sp_swap.
+ apply right_sym; auto with sets.
+
+ apply sp_swap.
+ apply left_sym; auto with sets.
+
+ apply sp_noswap.
+ apply right_sym; auto with sets.
+
+ apply sp_noswap.
+ apply left_sym; auto with sets.
 Qed.
 
 
-  Lemma Acc_swapprod: (x,y:A)(Acc A R x)->(Acc A R y)
-                                ->(Acc A*A SwapProd (x,y)).
+  Lemma Acc_swapprod :
+   forall x y:A, Acc R x -> Acc R y -> Acc SwapProd (x, y).
 Proof.
- NewInduction 1 as [x0 _ IHAcc0];Intros H2.
- Cut (y0:A)(R y0 x0)->(Acc ? SwapProd (y0,y)).
- Clear  IHAcc0.
- NewInduction H2 as [x1 _ IHAcc1]; Intros H4.
- Cut (y:A)(R y x1)->(Acc ? SwapProd (x0,y)).
- Clear  IHAcc1.
- Intro.
- Apply Acc_intro.
- NewDestruct y; Intro H5.
- Inversion_clear H5.
- Inversion_clear H0;Auto with sets.
-
- Apply swap_Acc.
- Inversion_clear H0;Auto with sets.
-
- Intros.
- Apply IHAcc1;Auto with sets;Intros.
- Apply Acc_inv with (y0,x1) ;Auto with sets.
- Apply sp_noswap.
- Apply right_sym;Auto with sets.
-
- Auto with sets.
+ induction 1 as [x0 _ IHAcc0]; intros H2.
+ cut (forall y0:A, R y0 x0 -> Acc SwapProd (y0, y)).
+ clear IHAcc0.
+ induction H2 as [x1 _ IHAcc1]; intros H4.
+ cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)).
+ clear IHAcc1.
+ intro.
+ apply Acc_intro.
+ destruct y; intro H5.
+ inversion_clear H5.
+ inversion_clear H0; auto with sets.
+
+ apply swap_Acc.
+ inversion_clear H0; auto with sets.
+
+ intros.
+ apply IHAcc1; auto with sets; intros.
+ apply Acc_inv with (y0, x1); auto with sets.
+ apply sp_noswap.
+ apply right_sym; auto with sets.
+
+ auto with sets.
 Qed.
 
 
-  Lemma wf_swapprod: (well_founded A R)->(well_founded A*A SwapProd).
+  Lemma wf_swapprod : well_founded R -> well_founded SwapProd.
 Proof.
- Red.
- NewDestruct a;Intros.
- Apply Acc_swapprod;Auto with sets.
+ red in |- *.
+ destruct a; intros.
+ apply Acc_swapprod; auto with sets.
 Qed.
 
-End Swap.
+End Swap.
\ No newline at end of file
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index c650d4675..b2af4dd85 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -10,38 +10,38 @@
 
 (** Author: Bruno Barras *)
 
-Require Relation_Definitions.
-Require Relation_Operators.
+Require Import Relation_Definitions.
+Require Import Relation_Operators.
 
 Section Wf_Transitive_Closure.
-  Variable A: Set.
-  Variable R: (relation A).
+  Variable A : Set.
+  Variable R : relation A.
 
   Notation trans_clos := (clos_trans A R).
  
-  Lemma incl_clos_trans: (inclusion A R trans_clos).
-    Red;Auto with sets.
+  Lemma incl_clos_trans : inclusion A R trans_clos.
+    red in |- *; auto with sets.
   Qed.
 
-  Lemma Acc_clos_trans: (x:A)(Acc A R x)->(Acc A trans_clos x).
-    NewInduction 1 as [x0 _ H1].
-    Apply Acc_intro.
-    Intros y H2.
-    NewInduction H2;Auto with sets.
-    Apply Acc_inv with y ;Auto with sets.
+  Lemma Acc_clos_trans : forall x:A, Acc R x -> Acc trans_clos x.
+    induction 1 as [x0 _ H1].
+    apply Acc_intro.
+    intros y H2.
+    induction H2; auto with sets.
+    apply Acc_inv with y; auto with sets.
   Qed.
 
-  Hints Resolve Acc_clos_trans.
+  Hint Resolve Acc_clos_trans.
 
-  Lemma Acc_inv_trans: (x,y:A)(trans_clos y x)->(Acc A R x)->(Acc A R y).
+  Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y.
   Proof.
-    NewInduction 1 as [|x y];Auto with sets.
-    Intro; Apply Acc_inv with y; Assumption.
+    induction 1 as [| x y]; auto with sets.
+    intro; apply Acc_inv with y; assumption.
   Qed.
 
-  Theorem wf_clos_trans: (well_founded A R)  ->(well_founded A trans_clos).
+  Theorem wf_clos_trans : well_founded R -> well_founded trans_clos.
   Proof.
-    Unfold well_founded;Auto with sets.
+    unfold well_founded in |- *; auto with sets.
   Qed.
 
-End Wf_Transitive_Closure.
+End Wf_Transitive_Closure.
\ No newline at end of file
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index ee45a9476..d7f241dd0 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -10,65 +10,68 @@
 
 (** Author: Bruno Barras *)
 
-Require Relation_Operators.
-Require Relation_Definitions.
-Require Transitive_Closure.
+Require Import Relation_Operators.
+Require Import Relation_Definitions.
+Require Import Transitive_Closure.
 
 Section WfUnion.
-  Variable A: Set.
-  Variable R1,R2: (relation A).
+  Variable A : Set.
+  Variables R1 R2 : relation A.
   
  Notation Union := (union A R1 R2).
 
- Hints Resolve Acc_clos_trans wf_clos_trans.
+ Hint Resolve Acc_clos_trans wf_clos_trans.
 
-Remark strip_commut: 
-      (commut A R1 R2)->(x,y:A)(clos_trans A R1 y x)->(z:A)(R2 z y)
-            ->(EX y':A | (R2 y' x) & (clos_trans A R1 z y')).
+Remark strip_commut :
+ commut A R1 R2 ->
+ forall x y:A,
+   clos_trans A R1 y x ->
+   forall z:A, R2 z y ->  exists2 y' : A | R2 y' x & clos_trans A R1 z y'.
 Proof.
- NewInduction 2 as [x y|x y z H0 IH1 H1 IH2]; Intros.
- Elim H with y x z ;Auto with sets;Intros x0 H2 H3.
- Exists x0;Auto with sets.
+ induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros.
+ elim H with y x z; auto with sets; intros x0 H2 H3.
+ exists x0; auto with sets.
 
- Elim IH1 with z0 ;Auto with sets;Intros.
- Elim IH2 with x0 ;Auto with sets;Intros.
- Exists x1;Auto with sets.
- Apply t_trans with x0; Auto with sets.
+ elim IH1 with z0; auto with sets; intros.
+ elim IH2 with x0; auto with sets; intros.
+ exists x1; auto with sets.
+ apply t_trans with x0; auto with sets.
 Qed.
 
 
-  Lemma Acc_union:  (commut A R1 R2)->((x:A)(Acc A R2 x)->(Acc A R1 x))
-                         ->(a:A)(Acc A R2 a)->(Acc A Union a).
+  Lemma Acc_union :
+   commut A R1 R2 ->
+   (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a.
 Proof.
- NewInduction 3 as [x H1 H2].
- Apply Acc_intro;Intros.
- Elim H3;Intros;Auto with sets.
- Cut (clos_trans A  R1 y x);Auto with sets.
- ElimType (Acc A (clos_trans A R1) y);Intros.
- Apply Acc_intro;Intros.
- Elim H8;Intros.
- Apply H6;Auto with sets.
- Apply t_trans with x0 ;Auto with sets.
+ induction 3 as [x H1 H2].
+ apply Acc_intro; intros.
+ elim H3; intros; auto with sets.
+ cut (clos_trans A R1 y x); auto with sets.
+ elimtype (Acc (clos_trans A R1) y); intros.
+ apply Acc_intro; intros.
+ elim H8; intros.
+ apply H6; auto with sets.
+ apply t_trans with x0; auto with sets.
 
- Elim strip_commut with x x0 y0 ;Auto with sets;Intros.
- Apply Acc_inv_trans with x1 ;Auto with sets.
- Unfold union .
- Elim H11;Auto with sets;Intros.
- Apply t_trans with y1 ;Auto with sets.
+ elim strip_commut with x x0 y0; auto with sets; intros.
+ apply Acc_inv_trans with x1; auto with sets.
+ unfold union in |- *.
+ elim H11; auto with sets; intros.
+ apply t_trans with y1; auto with sets.
 
- Apply (Acc_clos_trans A).
- Apply Acc_inv with x ;Auto with sets.
- Apply H0.
- Apply Acc_intro;Auto with sets.
+ apply (Acc_clos_trans A).
+ apply Acc_inv with x; auto with sets.
+ apply H0.
+ apply Acc_intro; auto with sets.
 Qed.
 
 
-  Theorem wf_union:  (commut A R1 R2)->(well_founded A R1)->(well_founded A R2)
-                  ->(well_founded A Union).
+  Theorem wf_union :
+   commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
 Proof.
- Unfold well_founded .
- Intros.
- Apply Acc_union;Auto with sets.
+ unfold well_founded in |- *.
+ intros.
+ apply Acc_union; auto with sets.
 Qed.
 
-End WfUnion.
+End WfUnion.
\ No newline at end of file
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index 49595dd2b..c4c7daa98 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -12,36 +12,36 @@
     From: Constructing Recursion Operators in Type Theory
     L. Paulson  JSC (1986) 2, 325-355 *)
 
-Require Eqdep.
+Require Import Eqdep.
 
 Section WellOrdering.
-Variable A:Set.
-Variable B:A->Set. 
+Variable A : Set.
+Variable B : A -> Set. 
 
 Inductive WO : Set :=
-   sup : (a:A)(f:(B a)->WO)WO.
+    sup : forall (a:A) (f:B a -> WO), WO.
 
 
-Inductive le_WO  : WO->WO->Prop :=
-  le_sup : (a:A)(f:(B a)->WO)(v:(B a)) (le_WO  (f v) (sup a f)).
+Inductive le_WO : WO -> WO -> Prop :=
+    le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f).
  
 
-Theorem wf_WO : (well_founded WO le_WO ).
+Theorem wf_WO : well_founded le_WO.
 Proof.
- Unfold well_founded ;Intro.
- Apply Acc_intro.
- Elim a.
- Intros.
- Inversion H0.
- Apply Acc_intro.
- Generalize H4 ;Generalize H1 ;Generalize f0 ;Generalize v.
- Rewrite -> H3.
- Intros.
- Apply (H v0 y0).
- Cut (eq ? f f1).
- Intros E;Rewrite -> E;Auto.
- Symmetry.
- Apply (inj_pair2 A [a0:A](B a0)->WO a0 f1 f H5).
+ unfold well_founded in |- *; intro.
+ apply Acc_intro.
+ elim a.
+ intros.
+ inversion H0.
+ apply Acc_intro.
+ generalize H4; generalize H1; generalize f0; generalize v.
+ rewrite H3.
+ intros.
+ apply (H v0 y0).
+ cut (f = f1).
+ intros E; rewrite E; auto.
+ symmetry  in |- *.
+ apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
 Qed.
 
 End WellOrdering.
@@ -53,20 +53,20 @@ Section Characterisation_wf_relations.
 (*  in course of development                                          *)
 
 
-Variable A:Set.
-Variable leA:A->A->Prop.
+Variable A : Set.
+Variable leA : A -> A -> Prop.
 
-Definition B:= [a:A] {x:A | (leA x a)}.
+Definition B (a:A) := {x : A | leA x a}.
 
-Definition  wof: (well_founded A leA)-> A-> (WO A B).
+Definition wof : well_founded leA -> A -> WO A B.
 Proof.
- Intros.
- Apply (well_founded_induction A leA H [a:A](WO A B));Auto.
- Intros.
- Apply (sup A B x).
- Unfold 1 B .
- NewDestruct 1 as [x0].
- Apply (H1 x0);Auto.
+ intros.
+ apply (well_founded_induction H (fun a:A => WO A B)); auto.
+ intros.
+ apply (sup A B x).
+ unfold B at 1 in |- *.
+ destruct 1 as [x0].
+ apply (H1 x0); auto.
 Qed.
 
-End Characterisation_wf_relations.
+End Characterisation_wf_relations.
\ No newline at end of file
diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v
index 10fca099c..65218643f 100644
--- a/theories/Wellfounded/Wellfounded.v
+++ b/theories/Wellfounded/Wellfounded.v
@@ -17,4 +17,3 @@ Require Export Transitive_Closure.
 Require Export Union.
 Require Export Well_Ordering.
 
-