Mise en forme des theories

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

7 files changed, 600 insertions, 625 deletions

diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 76c9ad443..c82549e37 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -15,41 +15,41 @@
 Require Import Relation_Operators.
 
 Section Wf_Disjoint_Union.
-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 : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
-Proof.
- induction 1.
- apply Acc_intro; intros y H2.
- inversion_clear H2.
- auto with sets.
-Qed.
-
-Lemma acc_B_sum :
- well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
-Proof.
- 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 leA -> well_founded leB -> well_founded Le_AsB.
-Proof.
- 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.
+  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 : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
+  Proof.
+    induction 1.
+    apply Acc_intro; intros y H2.
+    inversion_clear H2.
+    auto with sets.
+  Qed.
+
+  Lemma acc_B_sum :
+    well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
+  Proof.
+    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 leA -> well_founded leB -> well_founded Le_AsB.
+  Proof.
+    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.
\ No newline at end of file
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index 71bb8f507..7c69b6765 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -21,7 +21,7 @@ Section WfInclusion.
     induction 2.
     apply Acc_intro; auto with sets.
   Qed.
-
+  
   Hint Resolve Acc_incl.
 
   Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index e94a84b17..94ca69538 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -19,6 +19,7 @@ Section Inverse_Image.
   Let Rof (x y:A) : Prop := R (f x) (f y).
 
   Remark Acc_lemma : forall y:B, Acc R y -> forall x:A, y = f x -> Acc Rof x.
+  Proof.
     induction 1 as [y _ IHAcc]; intros x H.
     apply Acc_intro; intros y0 H1.
     apply (IHAcc (f y0)); try trivial.
@@ -26,30 +27,34 @@ Section Inverse_Image.
   Qed.
 
   Lemma Acc_inverse_image : forall x:A, Acc R (f x) -> Acc Rof x.
+  Proof.
     intros; apply (Acc_lemma (f x)); trivial.
   Qed.
 
   Theorem wf_inverse_image : well_founded R -> well_founded Rof.
+  Proof.
     red in |- *; intros; apply Acc_inverse_image; auto.
   Qed.
 
   Variable F : A -> B -> Prop.
   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 : 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 R -> well_founded RoF.
+    exists2 b : B, F x b & (forall c:B, F y c -> R b c).
+
+  Lemma Acc_inverse_rel : forall b:B, Acc R b -> forall x:A, F x b -> Acc RoF x.
+  Proof.
+    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 R -> well_founded RoF.
+  Proof.
     red in |- *; constructor; intros.
     case H0; intros.
     apply (Acc_inverse_rel x); auto.
-Qed.
+  Qed.
 
 End Inverse_Image.
 
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 387f69464..2604ccbee 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -19,356 +19,350 @@ Require Import Relation_Operators.
 Require Import Transitive_Closure.
 
 Section Wf_Lexicographic_Exponentiation.
-Variable A : Set.
-Variable leA : A -> A -> Prop.
-
-Notation Power := (Pow A leA).
-Notation Lex_Exp := (lex_exp A leA).
-Notation ltl := (Ltl A leA).
-Notation Descl := (Desc A leA).
-
-Notation List := (list A).
-Notation Nil := (nil (A:=A)).
-(* useless but symmetric *)
-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.
- 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 :
- 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 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 : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x.
-Proof.
- 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 :
- 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 := 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 :
- 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); 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 :
- forall x y:List, Descl (x ++ y) -> Descl x /\ Descl y.
-Proof.
-  intros.
-  apply (dist_aux (x ++ y) H x y); auto with sets.
-Qed.
-
-
-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 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 :
- 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).
-
- simpl in |- *; intros.
- inversion_clear H0.
- apply (Lt_hd A leA a b); auto with sets.
- 
- inversion_clear H1.
-Qed.
-
-
-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 (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)).
- auto with sets.
-
- unfold lex_exp in |- *; simpl in |- *; auto with sets.
-Qed.
-
-
-Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.
-Proof.
- 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.
+  Variable A : Set.
+  Variable leA : A -> A -> Prop.
+  
+  Notation Power := (Pow A leA).
+  Notation Lex_Exp := (lex_exp A leA).
+  Notation ltl := (Ltl A leA).
+  Notation Descl := (Desc A leA).
+  
+  Notation List := (list A).
+  Notation Nil := (nil (A:=A)).
+  (* useless but symmetric *)
+  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.
+    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 :
+    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 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 : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x.
+  Proof.
+    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 using d_nil with sets.
+    discriminate H5.
+    generalize (app_inj_tail _ _ _ _ H0).
+    simple induction 1; intros.
+    rewrite <- H4; auto with sets.
+  Qed.
+  
+  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 := 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 :
+    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); 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 :
+    forall x y:List, Descl (x ++ y) -> Descl x /\ Descl y.
+  Proof.
+    intros.
+    apply (dist_aux (x ++ y) H x y); auto with sets.
+  Qed.
+  
+  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 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 :
+    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).
+    
+    simpl in |- *; intros.
+    inversion_clear H0.
+    apply (Lt_hd A leA a b); auto with sets.
+    
+    inversion_clear H1.
+  Qed.
+  
+  
+  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 (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)).
+    auto with sets.
+    
+    unfold lex_exp in |- *; simpl in |- *; auto with sets.
+  Qed.
+  
+  
+  Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.
+  Proof.
+    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.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 94e97e6ee..82bede919 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -18,58 +18,56 @@ Require Import Transitive_Closure.
      L. Paulson  JSC (1986) 2, 325-355 *)
 
 Section WfLexicographic_Product.
-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).
-
-Hint Resolve t_step Acc_clos_trans wf_clos_trans.
-
-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.
- 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 leA ->
- (forall x:A, well_founded (leB x)) -> well_founded LexProd.
-Proof.
- 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.
+  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).
+  
+  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.
+    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 leA ->
+    (forall x:A, well_founded (leB x)) -> well_founded LexProd.
+  Proof.
+    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.
 
 
 End WfLexicographic_Product.
@@ -83,50 +81,31 @@ Section Wf_Symmetric_Product.
 
   Notation Symprod := (symprod A B leA leB).
 
-(*i
-  Local sig_prod:=
-         [x:A*B]<{_:A&B}>Case x of [a:A][b:B](existS A [_:A]B a b) end.
-
-Lemma incl_sym_lexprod: (included (A*B) Symprod  
-            (R_o_f (A*B) {_:A&B} sig_prod (lexprod A [_:A]B leA [_:A]leB))).
-Proof.
- Red.
- Induction x.
- (Induction y1;Intros).
- Red.
- Unfold sig_prod .
- Inversion_clear H.
- (Apply left_lex;Auto with sets).
-
- (Apply right_lex;Auto with sets).
-Qed.
-i*)
-
   Lemma Acc_symprod :
-   forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod (x, y).
- Proof.
- 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 leA -> well_founded leB -> well_founded Symprod.
-Proof.
- red in |- *.
- destruct a.
- apply Acc_symprod; auto with sets.
-Qed.
+    forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod (x, y).
+  Proof.
+    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 leA -> well_founded leB -> well_founded Symprod.
+  Proof.
+    red in |- *.
+    destruct a.
+    apply Acc_symprod; auto with sets.
+  Qed.
 
 End Wf_Symmetric_Product.
 
 
 Section Swap.
-
+  
   Variable A : Set.
   Variable R : A -> A -> Prop.
 
@@ -134,59 +113,59 @@ Section Swap.
 
 
   Lemma swap_Acc : forall x y:A, Acc SwapProd (x, y) -> Acc SwapProd (y, x).
-Proof.
- 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.
+  Proof.
+    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 :
-   forall x y:A, Acc R x -> Acc R y -> Acc SwapProd (x, y).
-Proof.
- 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.
-
-
+    forall x y:A, Acc R x -> Acc R y -> Acc SwapProd (x, y).
+  Proof.
+    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 R -> well_founded SwapProd.
-Proof.
- red in |- *.
- destruct a; intros.
- apply Acc_swapprod; auto with sets.
-Qed.
+  Proof.
+    red in |- *.
+    destruct a; intros.
+    apply Acc_swapprod; auto with sets.
+  Qed.
 
 End Swap.
\ No newline at end of file
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 17bde8c40..da1b78caa 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -18,60 +18,58 @@ Section WfUnion.
   Variable A : Set.
   Variables R1 R2 : relation A.
   
- Notation Union := (union A R1 R2).
-
- Hint Resolve Acc_clos_trans wf_clos_trans.
-
-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.
- 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.
-Qed.
+  Notation Union := (union A R1 R2).
+  
+  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.
+    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.
+  Qed.
 
 
   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.
- 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 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.
-Qed.
+    commut A R1 R2 ->
+    (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a.
+  Proof.
+    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 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.
+  Qed.
 
+  
   Theorem wf_union :
-   commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
-Proof.
- unfold well_founded in |- *.
- intros.
- apply Acc_union; auto with sets.
-Qed.
+    commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
+  Proof.
+    unfold well_founded in |- *.
+    intros.
+    apply Acc_union; auto with sets.
+  Qed.
 
 End WfUnion.
\ No newline at end of file
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index 03560253f..b1cb63be1 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -15,58 +15,57 @@
 Require Import Eqdep.
 
 Section WellOrdering.
-Variable A : Set.
-Variable B : A -> Set. 
-
-Inductive WO : Set :=
+  Variable A : Set.
+  Variable B : A -> Set. 
+  
+  Inductive WO : Set :=
     sup : forall (a:A) (f:B a -> WO), WO.
 
 
-Inductive le_WO : WO -> WO -> Prop :=
+  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 le_WO.
-Proof.
- 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.
+  Theorem wf_WO : well_founded le_WO.
+  Proof.
+    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.
 
 
 Section Characterisation_wf_relations.
 
-(** Wellfounded relations are the inverse image of wellordering types *)
-(*  in course of development                                          *)
+  (** Wellfounded relations are the inverse image of wellordering types *)
+  (*  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 leA -> A -> WO A B.
-Proof.
- 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.
+  Definition wof : well_founded leA -> A -> WO A B.
+  Proof.
+    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.
\ No newline at end of file