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

22 files changed, 1980 insertions, 1937 deletions

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index cd72483a3..e2d707367 100755
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -33,101 +33,100 @@ Require Export Classical_Type.
 (* Hints Unfold  not . *)
 
 Section Ensembles_classical.
-Variable U: Type.
+Variable U : Type.
 
-Lemma not_included_empty_Inhabited: 
-  (A: (Ensemble  U)) ~ (Included U A (Empty_set U)) -> (Inhabited U A).
+Lemma not_included_empty_Inhabited :
+ forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
 Proof.
-Intros A NI.
-Elim (not_all_ex_not U [x:U]~(In U A x)).
-Intros x H; Apply Inhabited_intro with x.
-Apply NNPP; Auto with sets.
-Red; Intro.
-Apply NI; Red.
-Intros x H'; Elim (H x); Trivial with sets.
+intros A NI.
+elim (not_all_ex_not U (fun x:U => ~ In U A x)).
+intros x H; apply Inhabited_intro with x.
+apply NNPP; auto with sets.
+red in |- *; intro.
+apply NI; red in |- *.
+intros x H'; elim (H x); trivial with sets.
 Qed.
-Hints Resolve not_included_empty_Inhabited.
+Hint Resolve not_included_empty_Inhabited.
 
-Lemma not_empty_Inhabited: 
-  (A: (Ensemble  U)) ~ A == (Empty_set U) -> (Inhabited U A).
+Lemma not_empty_Inhabited :
+ forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.
 Proof.
-Intros; Apply not_included_empty_Inhabited.
-Red; Auto with sets.
+intros; apply not_included_empty_Inhabited.
+red in |- *; auto with sets.
 Qed.
 
 Lemma Inhabited_Setminus :
-(X, Y: (Ensemble U)) (Included U X Y) -> ~ (Included U Y X) ->
-       (Inhabited U (Setminus U Y X)).
+ forall X Y:Ensemble U,
+   Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
 Proof.
-Intros X Y I NI. 
-Elim (not_all_ex_not U [x:U](In U Y x)->(In U X x) NI).
-Intros x YX.
-Apply Inhabited_intro with x.
-Apply Setminus_intro.
-Apply not_imply_elim with (In U X x); Trivial with sets.
-Auto with sets.
+intros X Y I NI. 
+elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
+intros x YX.
+apply Inhabited_intro with x.
+apply Setminus_intro.
+apply not_imply_elim with (In U X x); trivial with sets.
+auto with sets.
 Qed.
-Hints Resolve Inhabited_Setminus.
+Hint Resolve Inhabited_Setminus.
 
-Lemma Strict_super_set_contains_new_element:
-  (X, Y: (Ensemble U)) (Included U X Y) -> ~ X == Y ->
-   (Inhabited U (Setminus U Y X)).
+Lemma Strict_super_set_contains_new_element :
+ forall X Y:Ensemble U,
+   Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).
 Proof.
-Auto 7 with sets.
+auto 7 with sets.
 Qed.
-Hints Resolve Strict_super_set_contains_new_element.
+Hint Resolve Strict_super_set_contains_new_element.
 
-Lemma Subtract_intro:
-  (A: (Ensemble U)) (x, y: U) (In U A y) -> ~ x == y ->
-   (In U (Subtract U A x) y).
+Lemma Subtract_intro :
+ forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
 Proof.
-Unfold 1 Subtract; Auto with sets.
+unfold Subtract at 1 in |- *; auto with sets.
 Qed.
-Hints Resolve Subtract_intro.
+Hint Resolve Subtract_intro.
 
-Lemma Subtract_inv:
-  (A: (Ensemble U)) (x, y: U) (In U (Subtract U A x) y) ->
-   (In U A y) /\ ~ x == y.
+Lemma Subtract_inv :
+ forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
 Proof.
-Intros A x y H'; Elim H'; Auto with sets.
+intros A x y H'; elim H'; auto with sets.
 Qed.
 
-Lemma Included_Strict_Included:
-  (X, Y: (Ensemble U)) (Included U X Y) -> (Strict_Included U X Y) \/ X == Y.
+Lemma Included_Strict_Included :
+ forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.
 Proof.
-Intros X Y H'; Try Assumption.
-Elim (classic X == Y); Auto with sets.
+intros X Y H'; try assumption.
+elim (classic (X = Y)); auto with sets.
 Qed.
 
-Lemma Strict_Included_inv:
-  (X, Y: (Ensemble U)) (Strict_Included U X Y) ->
-   (Included U X Y) /\ (Inhabited U (Setminus U Y X)).
+Lemma Strict_Included_inv :
+ forall X Y:Ensemble U,
+   Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).
 Proof.
-Intros X Y H'; Red in H'.
-Split; [Tauto | Idtac].
-Elim H'; Intros H'0 H'1; Try Exact H'1; Clear H'.
-Apply Strict_super_set_contains_new_element; Auto with sets.
+intros X Y H'; red in H'.
+split; [ tauto | idtac ].
+elim H'; intros H'0 H'1; try exact H'1; clear H'.
+apply Strict_super_set_contains_new_element; auto with sets.
 Qed.
 
-Lemma not_SIncl_empty: 
-    (X: (Ensemble U)) ~ (Strict_Included U X (Empty_set U)).
+Lemma not_SIncl_empty :
+ forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
 Proof.
-Intro X; Red; Intro H'; Try Exact H'.
-LApply (Strict_Included_inv X (Empty_set U)); Auto with sets.
-Intro H'0; Elim H'0; Intros H'1 H'2; Elim H'2; Clear H'0.
-Intros x H'0; Elim H'0.
-Intro H'3; Elim H'3.
+intro X; red in |- *; intro H'; try exact H'.
+lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
+intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
+intros x H'0; elim H'0.
+intro H'3; elim H'3.
 Qed.
 
 Lemma Complement_Complement :
-  (A: (Ensemble U)) (Complement U (Complement U A)) == A.
+ forall A:Ensemble U, Complement U (Complement U A) = A.
 Proof.
-Unfold Complement; Intros; Apply Extensionality_Ensembles; Auto with sets.
-Red; Split; Auto with sets.
-Red; Intros; Apply NNPP; Auto with sets.
+unfold Complement in |- *; intros; apply Extensionality_Ensembles;
+ auto with sets.
+red in |- *; split; auto with sets.
+red in |- *; intros; apply NNPP; auto with sets.
 Qed.
 
 End Ensembles_classical.
 
-Hints Resolve Strict_super_set_contains_new_element Subtract_intro 
-	not_SIncl_empty : sets v62.
+Hint Resolve Strict_super_set_contains_new_element Subtract_intro
+  not_SIncl_empty: sets v62.
\ No newline at end of file
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 78ad3d2f2..b4250be92 100755
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -29,134 +29,131 @@
 Require Export Ensembles.
 
 Section Ensembles_facts.
-Variable U: Type.
+Variable U : Type.
 
-Lemma Extension: (B, C: (Ensemble U)) B == C -> (Same_set U B C).
+Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.
 Proof.
-Intros B C H'; Rewrite H'; Auto with sets.
+intros B C H'; rewrite H'; auto with sets.
 Qed.
 
-Lemma Noone_in_empty: (x: U) ~ (In U (Empty_set U) x).
+Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x.
 Proof.
-Red; NewDestruct 1.
+red in |- *; destruct 1.
 Qed.
-Hints Resolve Noone_in_empty.
+Hint Resolve Noone_in_empty.
 
-Lemma Included_Empty: (A: (Ensemble U))(Included U (Empty_set U) A).
+Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A.
 Proof.
-Intro; Red.
-Intros x H; Elim (Noone_in_empty x); Auto with sets.
+intro; red in |- *.
+intros x H; elim (Noone_in_empty x); auto with sets.
 Qed.
-Hints Resolve Included_Empty.
+Hint Resolve Included_Empty.
 
-Lemma Add_intro1:
-  (A: (Ensemble U)) (x, y: U) (In U A y) -> (In U (Add U A x) y).
+Lemma Add_intro1 :
+ forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y.
 Proof.
-Unfold 1 Add; Auto with sets.
+unfold Add at 1 in |- *; auto with sets.
 Qed.
-Hints Resolve Add_intro1.
+Hint Resolve Add_intro1.
 
-Lemma Add_intro2: (A: (Ensemble U)) (x: U) (In U (Add U A x) x).
+Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
 Proof.
-Unfold 1 Add; Auto with sets.
+unfold Add at 1 in |- *; auto with sets.
 Qed.
-Hints Resolve Add_intro2.
+Hint Resolve Add_intro2.
 
-Lemma Inhabited_add: (A: (Ensemble U)) (x: U) (Inhabited U (Add U A x)).
+Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x).
 Proof.
-Intros A x.
-Apply Inhabited_intro with x := x; Auto with sets.
+intros A x.
+apply Inhabited_intro with (x := x); auto with sets.
 Qed.
-Hints Resolve Inhabited_add.
+Hint Resolve Inhabited_add.
 
-Lemma Inhabited_not_empty:
-  (X: (Ensemble U)) (Inhabited U X) -> ~ X == (Empty_set U).
+Lemma Inhabited_not_empty :
+ forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.
 Proof.
-Intros X H'; Elim H'.
-Intros x H'0; Red; Intro H'1.
-Absurd (In U X x); Auto with sets.
-Rewrite H'1; Auto with sets.
+intros X H'; elim H'.
+intros x H'0; red in |- *; intro H'1.
+absurd (In U X x); auto with sets.
+rewrite H'1; auto with sets.
 Qed.
-Hints Resolve Inhabited_not_empty.
+Hint Resolve Inhabited_not_empty.
 
-Lemma Add_not_Empty :
- (A: (Ensemble U)) (x: U) ~ (Add U A x) == (Empty_set U).
+Lemma Add_not_Empty : forall (A:Ensemble U) (x:U), Add U A x <> Empty_set U.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
-Hints Resolve Add_not_Empty.
+Hint Resolve Add_not_Empty.
 
-Lemma not_Empty_Add :
- (A: (Ensemble U)) (x: U) ~ (Empty_set U) == (Add U A x).
+Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x.
 Proof.
-Intros; Red; Intro H; Generalize (Add_not_Empty A x); Auto with sets.
+intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets.
 Qed.
-Hints Resolve not_Empty_Add.
+Hint Resolve not_Empty_Add.
 
-Lemma Singleton_inv: (x, y: U) (In U (Singleton U x) y) -> x == y.
+Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y.
 Proof.
-Intros x y H'; Elim H'; Trivial with sets.
+intros x y H'; elim H'; trivial with sets.
 Qed.
-Hints Resolve Singleton_inv.
+Hint Resolve Singleton_inv.
 
-Lemma Singleton_intro: (x, y: U) x == y -> (In U (Singleton U x) y).
+Lemma Singleton_intro : forall x y:U, x = y -> In U (Singleton U x) y.
 Proof.
-Intros x y H'; Rewrite H'; Trivial with sets.
+intros x y H'; rewrite H'; trivial with sets.
 Qed.
-Hints Resolve Singleton_intro.
+Hint Resolve Singleton_intro.
 
-Lemma Union_inv:  (B, C: (Ensemble U)) (x: U) 
-  (In U (Union U B C) x) -> (In U B x) \/ (In U C x).
+Lemma Union_inv :
+ forall (B C:Ensemble U) (x:U), In U (Union U B C) x -> In U B x \/ In U C x.
 Proof.
-Intros B C x H'; Elim H'; Auto with sets.
+intros B C x H'; elim H'; auto with sets.
 Qed.
 
-Lemma Add_inv:
-  (A: (Ensemble U)) (x, y: U) (In U (Add U A x) y) -> (In U A y) \/ x == y.
+Lemma Add_inv :
+ forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
 Proof.
-Intros A x y H'; Elim H'; Auto with sets.
+intros A x y H'; elim H'; auto with sets.
 Qed.
 
-Lemma Intersection_inv:
-  (B, C: (Ensemble U)) (x: U) (In U (Intersection U B C) x) ->
-   (In U B x) /\ (In U C x).
+Lemma Intersection_inv :
+ forall (B C:Ensemble U) (x:U),
+   In U (Intersection U B C) x -> In U B x /\ In U C x.
 Proof.
-Intros B C x H'; Elim H'; Auto with sets.
+intros B C x H'; elim H'; auto with sets.
 Qed.
-Hints Resolve Intersection_inv.
+Hint Resolve Intersection_inv.
 
-Lemma Couple_inv: (x, y, z: U) (In U (Couple U x y) z) -> z == x \/ z == y.
+Lemma Couple_inv : forall x y z:U, In U (Couple U x y) z -> z = x \/ z = y.
 Proof.
-Intros x y z H'; Elim H'; Auto with sets.
+intros x y z H'; elim H'; auto with sets.
 Qed.
-Hints Resolve Couple_inv.
+Hint Resolve Couple_inv.
 
-Lemma Setminus_intro:
-  (A, B: (Ensemble U)) (x: U) (In U A x) -> ~ (In U B x) ->
-   (In U (Setminus U A B) x).
+Lemma Setminus_intro :
+ forall (A B:Ensemble U) (x:U),
+   In U A x -> ~ In U B x -> In U (Setminus U A B) x.
 Proof.
-Unfold 1 Setminus; Red; Auto with sets.
+unfold Setminus at 1 in |- *; red in |- *; auto with sets.
 Qed.
-Hints Resolve Setminus_intro.
+Hint Resolve Setminus_intro.
  
-Lemma Strict_Included_intro:
-  (X, Y: (Ensemble U)) (Included U X Y) /\ ~ X == Y -> 
-                       (Strict_Included U X Y).
+Lemma Strict_Included_intro :
+ forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
-Hints Resolve Strict_Included_intro.
+Hint Resolve Strict_Included_intro.
 
-Lemma Strict_Included_strict: (X: (Ensemble U)) ~ (Strict_Included U X X).
+Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X.
 Proof.
-Intro X; Red; Intro H'; Elim H'.
-Intros H'0 H'1; Elim H'1; Auto with sets.
+intro X; red in |- *; intro H'; elim H'.
+intros H'0 H'1; elim H'1; auto with sets.
 Qed.
-Hints Resolve Strict_Included_strict.
+Hint Resolve Strict_Included_strict.
 
 End Ensembles_facts.
 
-Hints Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2 
-	Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
-	Strict_Included_strict Noone_in_empty Inhabited_not_empty
-	Add_not_Empty  not_Empty_Add Inhabited_add Included_Empty : sets v62.
+Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
+  Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
+  Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
+  not_Empty_Add Inhabited_add Included_Empty: sets v62.
\ No newline at end of file
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index c234bd1c7..0d77c0617 100755
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -31,77 +31,79 @@ Require Export Relations_1.
 Require Export Partial_Order.
 
 Section Bounds.
-Variable U: Type.
-Variable D: (PO U).
+Variable U : Type.
+Variable D : PO U.
 
-Local C :=  (Carrier_of U D).
+Let C := Carrier_of U D.
 
-Local R :=  (Rel_of U D).
+Let R := Rel_of U D.
 
-Inductive Upper_Bound [B:(Ensemble U); x:U]: Prop :=
-      Upper_Bound_definition:
-        (In U C x) -> ((y: U) (In U B y) -> (R y x)) -> (Upper_Bound B x).
+Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
+    Upper_Bound_definition :
+      In U C x -> (forall y:U, In U B y -> R y x) -> Upper_Bound B x.
 
-Inductive Lower_Bound [B:(Ensemble U); x:U]: Prop :=
-      Lower_Bound_definition:
-        (In U C x) -> ((y: U) (In U B y) -> (R x y)) -> (Lower_Bound B x).
+Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
+    Lower_Bound_definition :
+      In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
 
-Inductive Lub [B:(Ensemble U); x:U]: Prop :=
-      Lub_definition:
-        (Upper_Bound B x) -> ((y: U) (Upper_Bound B y) -> (R x y)) -> (Lub B x).
+Inductive Lub (B:Ensemble U) (x:U) : Prop :=
+    Lub_definition :
+      Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
 
-Inductive Glb [B:(Ensemble U); x:U]: Prop :=
-      Glb_definition:
-        (Lower_Bound B x) -> ((y: U) (Lower_Bound B y) -> (R y x)) -> (Glb B x).
+Inductive Glb (B:Ensemble U) (x:U) : Prop :=
+    Glb_definition :
+      Lower_Bound B x -> (forall y:U, Lower_Bound B y -> R y x) -> Glb B x.
 
-Inductive Bottom [bot:U]: Prop :=
-      Bottom_definition:
-        (In U C bot) -> ((y: U) (In U C y) -> (R bot y)) -> (Bottom bot).
+Inductive Bottom (bot:U) : Prop :=
+    Bottom_definition :
+      In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
 
-Inductive Totally_ordered [B:(Ensemble U)]: Prop :=
-      Totally_ordered_definition:
-        ((Included U B C) ->
-          (x: U) (y: U) (Included U (Couple U x y) B) -> (R x y) \/ (R y x)) ->
-         (Totally_ordered B).
+Inductive Totally_ordered (B:Ensemble U) : Prop :=
+    Totally_ordered_definition :
+      (Included U B C ->
+       forall x y:U, Included U (Couple U x y) B -> R x y \/ R y x) ->
+      Totally_ordered B.
 
-Definition Compatible : (Relation U) :=
-   [x: U] [y: U] (In U C x) -> (In U C y) ->
-    (EXT z | (In U C z) /\ (Upper_Bound (Couple U x y) z)).
+Definition Compatible : Relation U :=
+  fun x y:U =>
+    In U C x ->
+    In U C y ->  exists z : _ | In U C z /\ Upper_Bound (Couple U x y) z.
 	
-Inductive Directed [X:(Ensemble U)]: Prop :=
-      Definition_of_Directed:
-        (Included U X C) ->
-        (Inhabited U X) ->
-        ((x1: U) (x2: U) (Included U (Couple U x1 x2) X) ->
-          (EXT x3 | (In U X x3) /\ (Upper_Bound (Couple U x1 x2) x3))) ->
-         (Directed X).
+Inductive Directed (X:Ensemble U) : Prop :=
+    Definition_of_Directed :
+      Included U X C ->
+      Inhabited U X ->
+      (forall x1 x2:U,
+         Included U (Couple U x1 x2) X ->
+          exists x3 : _ | In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
+      Directed X.
 
 Inductive Complete : Prop :=
-      Definition_of_Complete:
-        ((EXT bot | (Bottom bot))) ->
-        ((X: (Ensemble U)) (Directed X) -> (EXT bsup | (Lub X bsup))) ->
-         Complete.
+    Definition_of_Complete :
+      ( exists bot : _ | Bottom bot) ->
+      (forall X:Ensemble U, Directed X ->  exists bsup : _ | Lub X bsup) ->
+      Complete.
 
 Inductive Conditionally_complete : Prop :=
-      Definition_of_Conditionally_complete:
-        ((X: (Ensemble U))
-         (Included U X C) -> (EXT maj | (Upper_Bound X maj)) ->
-          (EXT bsup | (Lub X bsup))) -> Conditionally_complete.
+    Definition_of_Conditionally_complete :
+      (forall X:Ensemble U,
+         Included U X C ->
+         ( exists maj : _ | Upper_Bound X maj) ->
+          exists bsup : _ | Lub X bsup) -> Conditionally_complete.
 End Bounds.
-Hints Resolve Totally_ordered_definition Upper_Bound_definition 
-	Lower_Bound_definition Lub_definition Glb_definition
-	Bottom_definition Definition_of_Complete
-  	 Definition_of_Complete Definition_of_Conditionally_complete.
+Hint Resolve Totally_ordered_definition Upper_Bound_definition
+  Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
+  Definition_of_Complete Definition_of_Complete
+  Definition_of_Conditionally_complete.
 
 Section Specific_orders.
-Variable U: Type.
+Variable U : Type.
 
-Record Cpo : Type := Definition_of_cpo {
-   PO_of_cpo: (PO U);
-   Cpo_cond: (Complete U PO_of_cpo) }.
+Record Cpo : Type := Definition_of_cpo
+  {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
 
-Record Chain : Type := Definition_of_chain {
-   PO_of_chain: (PO U);
-   Chain_cond: (Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)) }.
+Record Chain : Type := Definition_of_chain
+  {PO_of_chain : PO U;
+   Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
 
-End Specific_orders.
+End Specific_orders.
\ No newline at end of file
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index af202239e..eae50a3d1 100755
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -27,20 +27,18 @@
 (*i $Id$ i*)
 
 Section Ensembles.
-Variable U: Type.
+Variable U : Type.
 
-Definition Ensemble :=  U -> Prop. 
+Definition Ensemble := U -> Prop. 
 
-Definition In : Ensemble -> U -> Prop :=  [A: Ensemble] [x: U] (A x).
+Definition In (A:Ensemble) (x:U) : Prop := A x.
 
-Definition Included : Ensemble -> Ensemble -> Prop :=
-   [B, C: Ensemble] (x: U) (In B x) -> (In C x).
+Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x.
 
-Inductive Empty_set : Ensemble :=
-   .
+Inductive Empty_set : Ensemble :=.
 
 Inductive Full_set : Ensemble :=
-     Full_intro: (x: U) (In Full_set x).
+    Full_intro : forall x:U, In Full_set x.
 
 (** NB: The following definition builds-in equality of elements in [U] as 
    Leibniz equality. 
@@ -49,60 +47,55 @@ Inductive Full_set : Ensemble :=
    with its own equality [eqs], with  
    [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
 
-Inductive Singleton [x:U] : Ensemble :=
-      In_singleton: (In (Singleton x) x).
+Inductive Singleton (x:U) : Ensemble :=
+    In_singleton : In (Singleton x) x.
 
-Inductive Union [B, C: Ensemble] : Ensemble :=
-     Union_introl: (x: U) (In B x) -> (In (Union B C) x)
-   | Union_intror: (x: U) (In C x) -> (In (Union B C) x).
+Inductive Union (B C:Ensemble) : Ensemble :=
+  | Union_introl : forall x:U, In B x -> In (Union B C) x
+  | Union_intror : forall x:U, In C x -> In (Union B C) x.
 
-Definition Add : Ensemble -> U -> Ensemble :=
-   [B: Ensemble] [x: U] (Union B (Singleton x)).
+Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x).
 
-Inductive Intersection [B, C:Ensemble] : Ensemble :=
-      Intersection_intro:
-        (x: U) (In B x) -> (In C x) -> (In (Intersection B C) x).
+Inductive Intersection (B C:Ensemble) : Ensemble :=
+    Intersection_intro :
+      forall x:U, In B x -> In C x -> In (Intersection B C) x.
 
-Inductive Couple [x,y:U] : Ensemble :=
-     Couple_l: (In (Couple x y) x)
-   | Couple_r: (In (Couple x y) y).
+Inductive Couple (x y:U) : Ensemble :=
+  | Couple_l : In (Couple x y) x
+  | Couple_r : In (Couple x y) y.
 
-Inductive Triple[x, y, z:U] : Ensemble :=
-    Triple_l: (In (Triple x y z) x)
-  | Triple_m: (In (Triple x y z) y)
-  | Triple_r: (In (Triple x y z) z).
+Inductive Triple (x y z:U) : Ensemble :=
+  | Triple_l : In (Triple x y z) x
+  | Triple_m : In (Triple x y z) y
+  | Triple_r : In (Triple x y z) z.
 
-Definition Complement : Ensemble -> Ensemble :=
-   [A: Ensemble] [x: U] ~ (In A x).
+Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x.
 
-Definition Setminus : Ensemble -> Ensemble -> Ensemble :=
-   [B: Ensemble] [C: Ensemble] [x: U] (In B x) /\ ~ (In C x).
+Definition Setminus (B C:Ensemble) : Ensemble :=
+  fun x:U => In B x /\ ~ In C x.
 
-Definition Subtract : Ensemble -> U -> Ensemble :=
-   [B: Ensemble] [x: U] (Setminus B (Singleton x)).
+Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x).
 
-Inductive Disjoint [B, C:Ensemble] : Prop :=
-      Disjoint_intro: ((x: U) ~ (In (Intersection B C) x)) -> (Disjoint B C).
+Inductive Disjoint (B C:Ensemble) : Prop :=
+    Disjoint_intro : (forall x:U, ~ In (Intersection B C) x) -> Disjoint B C.
 
-Inductive Inhabited [B:Ensemble] : Prop :=
-      Inhabited_intro: (x: U) (In B x) -> (Inhabited B).
+Inductive Inhabited (B:Ensemble) : Prop :=
+    Inhabited_intro : forall x:U, In B x -> Inhabited B.
 
-Definition Strict_Included : Ensemble -> Ensemble -> Prop :=
-   [B, C: Ensemble] (Included B C) /\ ~ B == C.
+Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C.
 
-Definition Same_set : Ensemble -> Ensemble -> Prop :=
-   [B, C: Ensemble] (Included B C) /\ (Included C B).
+Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B.
 
 (** Extensionality Axiom *)
 
-Axiom Extensionality_Ensembles:
-   (A,B: Ensemble) (Same_set A B) -> A == B.
-Hints Resolve Extensionality_Ensembles.
+Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.
+Hint Resolve Extensionality_Ensembles.
 
 End Ensembles.
 
-Hints Unfold In Included Same_set Strict_Included Add Setminus Subtract : sets v62.
+Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets
+  v62.
 
-Hints Resolve Union_introl Union_intror Intersection_intro In_singleton Couple_l
-	Couple_r Triple_l Triple_m Triple_r Disjoint_intro 
-	Extensionality_Ensembles : sets v62.
+Hint Resolve Union_introl Union_intror Intersection_intro In_singleton
+  Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro
+  Extensionality_Ensembles: sets v62.
\ No newline at end of file
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 1e7168791..28b2d6fb9 100755
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -26,49 +26,56 @@
 
 (*i $Id$ i*)
 
-Require Ensembles.
+Require Import Ensembles.
 
 Section Ensembles_finis.
-Variable U: Type.
+Variable U : Type.
 
-Inductive Finite : (Ensemble U) -> Prop :=
-      Empty_is_finite: (Finite (Empty_set U))
-   |  Union_is_finite:
-      (A: (Ensemble U)) (Finite A) -> 
-      (x: U) ~ (In U A x) -> (Finite (Add U A x)).
+Inductive Finite : Ensemble U -> Prop :=
+  | Empty_is_finite : Finite (Empty_set U)
+  | Union_is_finite :
+      forall A:Ensemble U,
+        Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).
 
-Inductive cardinal : (Ensemble U) -> nat -> Prop :=
-      card_empty: (cardinal (Empty_set U) O)
-   |  card_add:
-       (A: (Ensemble U)) (n: nat) (cardinal A n) ->
-        (x: U) ~ (In U A x) -> (cardinal (Add U A x) (S n)).
+Inductive cardinal : Ensemble U -> nat -> Prop :=
+  | card_empty : cardinal (Empty_set U) 0
+  | card_add :
+      forall (A:Ensemble U) (n:nat),
+        cardinal A n -> forall x:U, ~ In U A x -> cardinal (Add U A x) (S n).
 
 End Ensembles_finis.
 
-Hints Resolve Empty_is_finite Union_is_finite : sets v62.
-Hints Resolve card_empty card_add : sets v62.
+Hint Resolve Empty_is_finite Union_is_finite: sets v62.
+Hint Resolve card_empty card_add: sets v62.
 
-Require Constructive_sets.
+Require Import Constructive_sets.
 
 Section Ensembles_finis_facts.
-Variable U: Type.
+Variable U : Type.
 
 Lemma cardinal_invert :
- (X: (Ensemble U)) (p:nat)(cardinal U X p) -> Case p of
-           X == (Empty_set U)
-   [n:nat] (EXT A | (EXT x | 
-           X == (Add U A x) /\ ~ (In U A x) /\ (cardinal U A n))) end.
+ forall (X:Ensemble U) (p:nat),
+   cardinal U X p ->
+   match p with
+   | O => X = Empty_set U
+   | S n =>
+        exists A : _
+       | ( exists x : _ | X = Add U A x /\ ~ In U A x /\ cardinal U A n)
+   end.
 Proof.
-NewInduction 1; Simpl; Auto.
-Exists A; Exists x; Auto.
+induction 1; simpl in |- *; auto.
+exists A; exists x; auto.
 Qed.
 
 Lemma cardinal_elim :
- (X: (Ensemble U)) (p:nat)(cardinal U X p) -> Case p of
-                              X == (Empty_set U)
-                             [n:nat](Inhabited U X) end.
+ forall (X:Ensemble U) (p:nat),
+   cardinal U X p ->
+   match p with
+   | O => X = Empty_set U
+   | S n => Inhabited U X
+   end.
 Proof.
-Intros X p C; Elim C; Simpl; Trivial with sets.
+intros X p C; elim C; simpl in |- *; trivial with sets.
 Qed.
 
-End Ensembles_finis_facts.
+End Ensembles_finis_facts.
\ No newline at end of file
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 4e7b6931f..2849bce6c 100755
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -37,309 +37,311 @@ Require Export Gt.
 Require Export Lt.
 
 Section Finite_sets_facts.
-Variable U: Type.
+Variable U : Type.
 
 Lemma finite_cardinal :
- (X: (Ensemble U)) (Finite U X) -> (EX n:nat |(cardinal U X n)).
+ forall X:Ensemble U, Finite U X ->  exists n : nat | cardinal U X n.
 Proof.
-NewInduction 1 as [|A _ [n H]].
-Exists O; Auto with sets.
-Exists (S n); Auto with sets.
+induction 1 as [| A _ [n H]].
+exists 0; auto with sets.
+exists (S n); auto with sets.
 Qed.
 
-Lemma cardinal_finite:
-  (X: (Ensemble U)) (n: nat) (cardinal U X n) -> (Finite U X).
+Lemma cardinal_finite :
+ forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
 Proof.
-NewInduction 1; Auto with sets.
+induction 1; auto with sets.
 Qed.
 
-Theorem Add_preserves_Finite:
-  (X: (Ensemble U)) (x: U) (Finite U X) -> (Finite U (Add U X x)).
+Theorem Add_preserves_Finite :
+ forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
 Proof.
-Intros X x H'.
-Elim (classic (In U X x)); Intro H'0; Auto with sets.
-Rewrite (Non_disjoint_union U X x); Auto with sets.
+intros X x H'.
+elim (classic (In U X x)); intro H'0; auto with sets.
+rewrite (Non_disjoint_union U X x); auto with sets.
 Qed.
-Hints Resolve Add_preserves_Finite.
+Hint Resolve Add_preserves_Finite.
 
-Theorem Singleton_is_finite: (x: U) (Finite U (Singleton U x)).
+Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
 Proof.
-Intro x; Rewrite <- (Empty_set_zero U (Singleton U x)).
-Change (Finite U (Add U (Empty_set U) x)); Auto with sets.
+intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
+change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
 Qed.
-Hints Resolve Singleton_is_finite.
+Hint Resolve Singleton_is_finite.
 
-Theorem Union_preserves_Finite:
-  (X, Y: (Ensemble U)) (Finite U X) -> (Finite U Y) -> 
-                       (Finite U (Union U X Y)).
+Theorem Union_preserves_Finite :
+ forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
 Proof.
-Intros X Y H'; Elim H'.
-Rewrite (Empty_set_zero U Y); Auto with sets.
-Intros A H'0 H'1 x H'2 H'3.
-Rewrite (Union_commutative U (Add U A x) Y).
-Rewrite <- (Union_add U Y A x).
-Rewrite (Union_commutative U Y A); Auto with sets.
+intros X Y H'; elim H'.
+rewrite (Empty_set_zero U Y); auto with sets.
+intros A H'0 H'1 x H'2 H'3.
+rewrite (Union_commutative U (Add U A x) Y).
+rewrite <- (Union_add U Y A x).
+rewrite (Union_commutative U Y A); auto with sets.
 Qed.
 
-Lemma Finite_downward_closed:
-  (A: (Ensemble U)) (Finite U A) ->
-   (X: (Ensemble U)) (Included U X A) -> (Finite U X).
+Lemma Finite_downward_closed :
+ forall A:Ensemble U,
+   Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
 Proof.
-Intros A H'; Elim H'; Auto with sets.
-Intros X H'0.
-Rewrite (less_than_empty U X H'0); Auto with sets.
-Intros; Elim Included_Add with U X A0 x; Auto with sets.
-NewDestruct 1 as [A' [H5 H6]].
-Rewrite H5; Auto with sets.
+intros A H'; elim H'; auto with sets.
+intros X H'0.
+rewrite (less_than_empty U X H'0); auto with sets.
+intros; elim Included_Add with U X A0 x; auto with sets.
+destruct 1 as [A' [H5 H6]].
+rewrite H5; auto with sets.
 Qed.
 
-Lemma Intersection_preserves_finite:
-  (A: (Ensemble U)) (Finite U A) ->
-   (X: (Ensemble U)) (Finite U (Intersection U X A)).
+Lemma Intersection_preserves_finite :
+ forall A:Ensemble U,
+   Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
 Proof.
-Intros A H' X; Apply Finite_downward_closed with A; Auto with sets.
+intros A H' X; apply Finite_downward_closed with A; auto with sets.
 Qed.
 
-Lemma cardinalO_empty:
-  (X: (Ensemble U)) (cardinal U X O) -> X == (Empty_set U).
+Lemma cardinalO_empty :
+ forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
 Proof.
-Intros X H; Apply (cardinal_invert U X O); Trivial with sets.
+intros X H; apply (cardinal_invert U X 0); trivial with sets.
 Qed.
-Hints Resolve cardinalO_empty.
+Hint Resolve cardinalO_empty.
 
-Lemma inh_card_gt_O:
-  (X: (Ensemble U)) (Inhabited U X) -> (n: nat) (cardinal U X n) -> (gt n O).
+Lemma inh_card_gt_O :
+ forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
 Proof.
-NewInduction 1 as [x H'].
-Intros n H'0.
-Elim (gt_O_eq n); Auto with sets.
-Intro H'1; Generalize H'; Generalize H'0.
-Rewrite <- H'1; Intro H'2.
-Rewrite (cardinalO_empty X); Auto with sets.
-Intro H'3; Elim H'3.
+induction 1 as [x H'].
+intros n H'0.
+elim (gt_O_eq n); auto with sets.
+intro H'1; generalize H'; generalize H'0.
+rewrite <- H'1; intro H'2.
+rewrite (cardinalO_empty X); auto with sets.
+intro H'3; elim H'3.
 Qed.
 
-Lemma card_soustr_1:
-  (X: (Ensemble U)) (n: nat) (cardinal U X n) ->
-   (x: U) (In U X x) -> (cardinal U (Subtract U X x) (pred n)).
+Lemma card_soustr_1 :
+ forall (X:Ensemble U) (n:nat),
+   cardinal U X n ->
+   forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
 Proof.
-Intros X n H'; Elim H'.
-Intros x H'0; Elim H'0.
-Clear H' n X.
-Intros X n H' H'0 x H'1 x0 H'2.
-Elim (classic (In U X x0)).
-Intro H'4; Rewrite (add_soustr_xy U X x x0).
-Elim (classic x == x0).
-Intro H'5.
-Absurd (In U X x0); Auto with sets.
-Rewrite <- H'5; Auto with sets.
-Intro H'3; Try Assumption.
-Cut (S (pred n)) = (pred (S n)).
-Intro H'5; Rewrite <- H'5.
-Apply card_add; Auto with sets.
-Red; Intro H'6; Elim H'6.
-Intros H'7 H'8; Try Assumption.
-Elim H'1; Auto with sets.
-Unfold 2 pred; Symmetry.
-Apply S_pred with m := O.
-Change (gt n O).
-Apply inh_card_gt_O with X := X; Auto with sets.
-Apply Inhabited_intro with x := x0; Auto with sets.
-Red; Intro H'3.
-Apply H'1.
-Elim H'3; Auto with sets.
-Rewrite H'3; Auto with sets.
-Elim (classic x == x0).
-Intro H'3; Rewrite <- H'3.
-Cut (Subtract U (Add U X x) x) == X; Auto with sets.
-Intro H'4; Rewrite H'4; Auto with sets.
-Intros H'3 H'4; Try Assumption.
-Absurd (In U (Add U X x) x0); Auto with sets.
-Red; Intro H'5; Try Exact H'5.
-LApply (Add_inv U X x x0); Tauto.
+intros X n H'; elim H'.
+intros x H'0; elim H'0.
+clear H' n X.
+intros X n H' H'0 x H'1 x0 H'2.
+elim (classic (In U X x0)).
+intro H'4; rewrite (add_soustr_xy U X x x0).
+elim (classic (x = x0)).
+intro H'5.
+absurd (In U X x0); auto with sets.
+rewrite <- H'5; auto with sets.
+intro H'3; try assumption.
+cut (S (pred n) = pred (S n)).
+intro H'5; rewrite <- H'5.
+apply card_add; auto with sets.
+red in |- *; intro H'6; elim H'6.
+intros H'7 H'8; try assumption.
+elim H'1; auto with sets.
+unfold pred at 2 in |- *; symmetry  in |- *.
+apply S_pred with (m := 0).
+change (n > 0) in |- *.
+apply inh_card_gt_O with (X := X); auto with sets.
+apply Inhabited_intro with (x := x0); auto with sets.
+red in |- *; intro H'3.
+apply H'1.
+elim H'3; auto with sets.
+rewrite H'3; auto with sets.
+elim (classic (x = x0)).
+intro H'3; rewrite <- H'3.
+cut (Subtract U (Add U X x) x = X); auto with sets.
+intro H'4; rewrite H'4; auto with sets.
+intros H'3 H'4; try assumption.
+absurd (In U (Add U X x) x0); auto with sets.
+red in |- *; intro H'5; try exact H'5.
+lapply (Add_inv U X x x0); tauto.
 Qed.
 
-Lemma cardinal_is_functional:
-  (X: (Ensemble U)) (c1: nat) (cardinal U X c1) ->
-   (Y: (Ensemble U)) (c2: nat) (cardinal U Y c2) -> X == Y ->
-    c1 = c2.
+Lemma cardinal_is_functional :
+ forall (X:Ensemble U) (c1:nat),
+   cardinal U X c1 ->
+   forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
 Proof.
-Intros X c1 H'; Elim H'.
-Intros Y c2 H'0; Elim H'0; Auto with sets.
-Intros A n H'1 H'2 x H'3 H'5.
-Elim (not_Empty_Add U A x); Auto with sets.
-Clear H' c1 X.
-Intros X n H' H'0 x H'1 Y c2 H'2.
-Elim H'2.
-Intro H'3.
-Elim (not_Empty_Add U X x); Auto with sets.
-Clear H'2 c2 Y.
-Intros X0 c2 H'2 H'3 x0 H'4 H'5.
-Elim (classic (In U X0 x)).
-Intro H'6; Apply f_equal with nat.
-Apply H'0 with Y := (Subtract U (Add U X0 x0) x).
-ElimType (pred (S c2)) = c2; Auto with sets.
-Apply card_soustr_1; Auto with sets.
-Rewrite <- H'5.
-Apply Sub_Add_new; Auto with sets.
-Elim (classic x == x0).
-Intros H'6 H'7; Apply f_equal with nat.
-Apply H'0 with Y := X0; Auto with sets.
-Apply Simplify_add with x := x; Auto with sets.
-Pattern 2 x; Rewrite H'6; Auto with sets.
-Intros H'6 H'7.
-Absurd (Add U X x) == (Add U X0 x0); Auto with sets.
-Clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
-Red; Intro H'.
-LApply (Extension U (Add U X x) (Add U X0 x0)); Auto with sets.
-Clear H'.
-Intro H'; Red in H'.
-Elim H'; Intros H'0 H'1; Red in H'0; Clear H' H'1.
-Absurd (In U (Add U X0 x0) x); Auto with sets.
-LApply (Add_inv U X0 x0 x); [ Intuition | Apply (H'0 x); Apply Add_intro2 ].
+intros X c1 H'; elim H'.
+intros Y c2 H'0; elim H'0; auto with sets.
+intros A n H'1 H'2 x H'3 H'5.
+elim (not_Empty_Add U A x); auto with sets.
+clear H' c1 X.
+intros X n H' H'0 x H'1 Y c2 H'2.
+elim H'2.
+intro H'3.
+elim (not_Empty_Add U X x); auto with sets.
+clear H'2 c2 Y.
+intros X0 c2 H'2 H'3 x0 H'4 H'5.
+elim (classic (In U X0 x)).
+intro H'6; apply f_equal with nat.
+apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+elimtype (pred (S c2) = c2); auto with sets.
+apply card_soustr_1; auto with sets.
+rewrite <- H'5.
+apply Sub_Add_new; auto with sets.
+elim (classic (x = x0)).
+intros H'6 H'7; apply f_equal with nat.
+apply H'0 with (Y := X0); auto with sets.
+apply Simplify_add with (x := x); auto with sets.
+pattern x at 2 in |- *; rewrite H'6; auto with sets.
+intros H'6 H'7.
+absurd (Add U X x = Add U X0 x0); auto with sets.
+clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
+red in |- *; intro H'.
+lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
+clear H'.
+intro H'; red in H'.
+elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
+absurd (In U (Add U X0 x0) x); auto with sets.
+lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
 Qed.
 
-Lemma cardinal_Empty : (m:nat)(cardinal U (Empty_set U) m) -> O = m.
+Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
 Proof.
-Intros m Cm; Generalize (cardinal_invert U (Empty_set U) m Cm).
-Elim m; Auto with sets.
-Intros; Elim H0; Intros; Elim H1; Intros; Elim H2; Intros.
-Elim (not_Empty_Add U x x0 H3).
+intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
+elim m; auto with sets.
+intros; elim H0; intros; elim H1; intros; elim H2; intros.
+elim (not_Empty_Add U x x0 H3).
 Qed.
 
 Lemma cardinal_unicity :
-  (X: (Ensemble U)) (n: nat) (cardinal U X n) -> 
-                    (m: nat) (cardinal U X m) -> n = m.
+ forall (X:Ensemble U) (n:nat),
+   cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
 Proof.
-Intros; Apply cardinal_is_functional with X X; Auto with sets.
+intros; apply cardinal_is_functional with X X; auto with sets.
 Qed.
 
-Lemma card_Add_gen:
-  (A: (Ensemble U))
-  (x: U) (n, n': nat) (cardinal U A n) -> (cardinal U (Add U A x) n') ->
-   (le n' (S n)).
+Lemma card_Add_gen :
+ forall (A:Ensemble U) (x:U) (n n':nat),
+   cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
 Proof.
-Intros A x n n' H'.
-Elim (classic (In U A x)).
-Intro H'0.
-Rewrite (Non_disjoint_union U A x H'0).
-Intro H'1; Cut n = n'.
-Intro E; Rewrite E; Auto with sets.
-Apply cardinal_unicity with A; Auto with sets.
-Intros H'0 H'1.
-Cut n'=(S n).
-Intro E; Rewrite E; Auto with sets.
-Apply cardinal_unicity with (Add U A x); Auto with sets.
+intros A x n n' H'.
+elim (classic (In U A x)).
+intro H'0.
+rewrite (Non_disjoint_union U A x H'0).
+intro H'1; cut (n = n').
+intro E; rewrite E; auto with sets.
+apply cardinal_unicity with A; auto with sets.
+intros H'0 H'1.
+cut (n' = S n).
+intro E; rewrite E; auto with sets.
+apply cardinal_unicity with (Add U A x); auto with sets.
 Qed.
 
-Lemma incl_st_card_lt:
-  (X: (Ensemble U)) (c1: nat) (cardinal U X c1) ->
-  (Y: (Ensemble U)) (c2: nat) (cardinal U Y c2) -> (Strict_Included U X Y) ->
-    (gt c2 c1).
+Lemma incl_st_card_lt :
+ forall (X:Ensemble U) (c1:nat),
+   cardinal U X c1 ->
+   forall (Y:Ensemble U) (c2:nat),
+     cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
 Proof.
-Intros X c1 H'; Elim H'.
-Intros Y c2 H'0; Elim H'0; Auto with sets arith.
-Intro H'1.
-Elim (Strict_Included_strict U (Empty_set U)); Auto with sets arith.
-Clear H' c1 X.
-Intros X n H' H'0 x H'1 Y c2 H'2.
-Elim H'2.
-Intro H'3; Elim (not_SIncl_empty U (Add U X x)); Auto with sets arith.
-Clear H'2 c2 Y.
-Intros X0 c2 H'2 H'3 x0 H'4 H'5; Elim (classic (In U X0 x)).
-Intro H'6; Apply gt_n_S.
-Apply H'0 with Y := (Subtract U (Add U X0 x0) x).
-ElimType (pred (S c2)) = c2; Auto with sets arith.
-Apply card_soustr_1; Auto with sets arith.
-Apply incl_st_add_soustr; Auto with sets arith.
-Elim (classic x == x0).
-Intros H'6 H'7; Apply gt_n_S.
-Apply H'0 with Y := X0; Auto with sets arith.
-Apply sincl_add_x with x := x0.
-Rewrite <- H'6; Auto with sets arith.
-Pattern 1 x0; Rewrite <- H'6; Trivial with sets arith.
-Intros H'6 H'7; Red in H'5.
-Elim H'5; Intros H'8 H'9; Try Exact H'8; Clear H'5.
-Red in H'8.
-Generalize (H'8 x).
-Intro H'5; LApply H'5; Auto with sets arith.
-Intro H; Elim Add_inv with U X0 x0 x; Auto with sets arith.
-Intro; Absurd (In U X0 x); Auto with sets arith.
-Intro; Absurd x==x0; Auto with sets arith.
+intros X c1 H'; elim H'.
+intros Y c2 H'0; elim H'0; auto with sets arith.
+intro H'1.
+elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
+clear H' c1 X.
+intros X n H' H'0 x H'1 Y c2 H'2.
+elim H'2.
+intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
+clear H'2 c2 Y.
+intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
+intro H'6; apply gt_n_S.
+apply H'0 with (Y := Subtract U (Add U X0 x0) x).
+elimtype (pred (S c2) = c2); auto with sets arith.
+apply card_soustr_1; auto with sets arith.
+apply incl_st_add_soustr; auto with sets arith.
+elim (classic (x = x0)).
+intros H'6 H'7; apply gt_n_S.
+apply H'0 with (Y := X0); auto with sets arith.
+apply sincl_add_x with (x := x0).
+rewrite <- H'6; auto with sets arith.
+pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
+intros H'6 H'7; red in H'5.
+elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
+red in H'8.
+generalize (H'8 x).
+intro H'5; lapply H'5; auto with sets arith.
+intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
+intro; absurd (In U X0 x); auto with sets arith.
+intro; absurd (x = x0); auto with sets arith.
 Qed.
 
-Lemma incl_card_le:
-  (X,Y: (Ensemble U)) (n,m: nat) (cardinal U X n) -> (cardinal U Y m) -> 
-  (Included U X Y) -> (le n m).
+Lemma incl_card_le :
+ forall (X Y:Ensemble U) (n m:nat),
+   cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
 Proof.
-Intros;
-Elim Included_Strict_Included with U X Y; Auto with sets arith; Intro.
-Cut (gt m n); Auto with sets arith.
-Apply incl_st_card_lt with X := X Y := Y; Auto with sets arith.
-Generalize H0; Rewrite <- H2; Intro.
-Cut n=m.
-Intro E; Rewrite E; Auto with sets arith.
-Apply cardinal_unicity with X; Auto with sets arith.
+intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
+cut (m > n); auto with sets arith.
+apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
+generalize H0; rewrite <- H2; intro.
+cut (n = m).
+intro E; rewrite E; auto with sets arith.
+apply cardinal_unicity with X; auto with sets arith.
 Qed.
 
-Lemma G_aux:
-  (P:(Ensemble U) ->Prop)
-  ((X:(Ensemble U))
-   (Finite U X) -> ((Y:(Ensemble U)) (Strict_Included U Y X) ->(P Y)) ->(P X)) ->
-  (P (Empty_set U)).
+Lemma G_aux :
+ forall P:Ensemble U -> Prop,
+   (forall X:Ensemble U,
+      Finite U X ->
+      (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+   P (Empty_set U).
 Proof.
-Intros P H'; Try Assumption.
-Apply H'; Auto with sets.
-Clear H'; Auto with sets.
-Intros Y H'; Try Assumption.
-Red in H'.
-Elim H'; Intros H'0 H'1; Try Exact H'1; Clear H'.
-LApply (less_than_empty U Y); [Intro H'3; Try Exact H'3 | Assumption].
-Elim H'1; Auto with sets.
+intros P H'; try assumption.
+apply H'; auto with sets.
+clear H'; auto with sets.
+intros Y H'; try assumption.
+red in H'.
+elim H'; intros H'0 H'1; try exact H'1; clear H'.
+lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
+elim H'1; auto with sets.
 Qed.
 
-Hints Unfold  not.
+Hint Unfold not.
 
-Lemma Generalized_induction_on_finite_sets:
-  (P:(Ensemble U) ->Prop)
-  ((X:(Ensemble U))
-   (Finite U X) -> ((Y:(Ensemble U)) (Strict_Included U Y X) ->(P Y)) ->(P X)) ->
-  (X:(Ensemble U)) (Finite U X) ->(P X).
+Lemma Generalized_induction_on_finite_sets :
+ forall P:Ensemble U -> Prop,
+   (forall X:Ensemble U,
+      Finite U X ->
+      (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
+   forall X:Ensemble U, Finite U X -> P X.
 Proof.
-Intros P H'0 X H'1.
-Generalize P H'0; Clear H'0 P.
-Elim H'1.
-Intros P H'0.
-Apply G_aux; Auto with sets.
-Clear H'1 X.
-Intros A H' H'0 x H'1 P H'3.
-Cut (Y:(Ensemble U)) (Included U Y (Add U A x)) ->(P Y); Auto with sets.
-Generalize H'1.
-Apply H'0.
-Intros X K H'5 L Y H'6; Apply H'3; Auto with sets.
-Apply Finite_downward_closed with A := (Add U X x); Auto with sets.
-Intros Y0 H'7.
-Elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x)); Auto with sets.
-Intros H'2 H'4.
-Elim (Included_Add U Y0 X x);
- [Intro H'14 |
-   Intro H'14; Elim H'14; Intros A' E; Elim E; Intros H'15 H'16; Clear E H'14 |
-   Idtac]; Auto with sets.
-Elim (Included_Strict_Included U Y0 X); Auto with sets.
-Intro H'9; Apply H'5 with Y := Y0; Auto with sets.
-Intro H'9; Rewrite H'9.
-Apply H'3; Auto with sets.
-Intros Y1 H'8; Elim H'8.
-Intros H'10 H'11; Apply H'5 with Y := Y1; Auto with sets.
-Elim (Included_Strict_Included U A' X); Auto with sets.
-Intro H'8; Apply H'5 with Y := A'; Auto with sets.
-Rewrite <- H'15; Auto with sets.
-Intro H'8.
-Elim H'7.
-Intros H'9 H'10; Apply H'10 Orelse Elim H'10; Try Assumption.
-Generalize H'6.
-Rewrite <- H'8.
-Rewrite <- H'15; Auto with sets.
+intros P H'0 X H'1.
+generalize P H'0; clear H'0 P.
+elim H'1.
+intros P H'0.
+apply G_aux; auto with sets.
+clear H'1 X.
+intros A H' H'0 x H'1 P H'3.
+cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
+generalize H'1.
+apply H'0.
+intros X K H'5 L Y H'6; apply H'3; auto with sets.
+apply Finite_downward_closed with (A := Add U X x); auto with sets.
+intros Y0 H'7.
+elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
+ auto with sets.
+intros H'2 H'4.
+elim (Included_Add U Y0 X x);
+ [ intro H'14
+ | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
+ | idtac ]; auto with sets.
+elim (Included_Strict_Included U Y0 X); auto with sets.
+intro H'9; apply H'5 with (Y := Y0); auto with sets.
+intro H'9; rewrite H'9.
+apply H'3; auto with sets.
+intros Y1 H'8; elim H'8.
+intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
+elim (Included_Strict_Included U A' X); auto with sets.
+intro H'8; apply H'5 with (Y := A'); auto with sets.
+rewrite <- H'15; auto with sets.
+intro H'8.
+elim H'7.
+intros H'9 H'10; apply H'10 || elim H'10; try assumption.
+generalize H'6.
+rewrite <- H'8.
+rewrite <- H'15; auto with sets.
 Qed.
 
-End Finite_sets_facts.
+End Finite_sets_facts.
\ No newline at end of file
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index d5f42e3f9..85b83d3ab 100755
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -39,161 +39,167 @@ Require Export Le.
 Require Export Finite_sets_facts.
 
 Section Image.
-Variables U, V: Type.
+Variables U V : Type.
 
-Inductive Im [X:(Ensemble U); f:U -> V]: (Ensemble V) :=
-      Im_intro: (x: U) (In ? X x) -> (y: V) y == (f x) -> (In ? (Im X f) y).
+Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V :=
+    Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y.
 
-Lemma Im_def:
-  (X: (Ensemble U)) (f: U -> V) (x: U) (In ? X x) -> (In ? (Im X f) (f x)).
+Lemma Im_def :
+ forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x).
 Proof.
-Intros X f x H'; Try Assumption.
-Apply Im_intro with x := x; Auto with sets.
+intros X f x H'; try assumption.
+apply Im_intro with (x := x); auto with sets.
 Qed.
-Hints Resolve Im_def.
+Hint Resolve Im_def.
 
-Lemma Im_add:
-  (X: (Ensemble U)) (x: U) (f: U -> V)
-      (Im (Add ? X x) f) == (Add ? (Im X f) (f x)).
+Lemma Im_add :
+ forall (X:Ensemble U) (x:U) (f:U -> V),
+   Im (Add _ X x) f = Add _ (Im X f) (f x).
 Proof.
-Intros X x f.
-Apply Extensionality_Ensembles.
-Split; Red; Intros x0 H'.
-Elim H'; Intros.
-Rewrite H0.
-Elim Add_inv with U X x x1; Auto with sets.
-NewDestruct 1; Auto with sets.
-Elim Add_inv with V (Im X f) (f x) x0; Auto with sets.
-NewDestruct 1 as [x0 H y H0].
-Rewrite H0; Auto with sets.
-NewDestruct 1; Auto with sets.
+intros X x f.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x0 H'.
+elim H'; intros.
+rewrite H0.
+elim Add_inv with U X x x1; auto with sets.
+destruct 1; auto with sets.
+elim Add_inv with V (Im X f) (f x) x0; auto with sets.
+destruct 1 as [x0 H y H0].
+rewrite H0; auto with sets.
+destruct 1; auto with sets.
 Qed.
 
-Lemma image_empty: (f: U -> V) (Im (Empty_set U) f) == (Empty_set V).
+Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
 Proof.
-Intro f; Try Assumption.
-Apply Extensionality_Ensembles.
-Split; Auto with sets.
-Red.
-Intros x H'; Elim H'.
-Intros x0 H'0; Elim H'0; Auto with sets.
+intro f; try assumption.
+apply Extensionality_Ensembles.
+split; auto with sets.
+red in |- *.
+intros x H'; elim H'.
+intros x0 H'0; elim H'0; auto with sets.
 Qed.
-Hints Resolve image_empty.
+Hint Resolve image_empty.
 
-Lemma finite_image:
-  (X: (Ensemble U)) (f: U -> V) (Finite ? X) -> (Finite ? (Im X f)).
+Lemma finite_image :
+ forall (X:Ensemble U) (f:U -> V), Finite _ X -> Finite _ (Im X f).
 Proof.
-Intros X f H'; Elim H'.
-Rewrite (image_empty f); Auto with sets.
-Intros A H'0 H'1 x H'2; Clear H' X.
-Rewrite (Im_add A x f); Auto with sets.
-Apply Add_preserves_Finite; Auto with sets.
+intros X f H'; elim H'.
+rewrite (image_empty f); auto with sets.
+intros A H'0 H'1 x H'2; clear H' X.
+rewrite (Im_add A x f); auto with sets.
+apply Add_preserves_Finite; auto with sets.
 Qed.
-Hints Resolve finite_image.
+Hint Resolve finite_image.
 
-Lemma Im_inv:
-  (X: (Ensemble U)) (f: U -> V) (y: V) (In ? (Im X f) y) ->
-   (exT ? [x: U] (In ? X x) /\ (f x) == y).
+Lemma Im_inv :
+ forall (X:Ensemble U) (f:U -> V) (y:V),
+   In _ (Im X f) y ->  exists x : U | In _ X x /\ f x = y.
 Proof.
-Intros X f y H'; Elim H'.
-Intros x H'0 y0 H'1; Rewrite H'1.
-Exists x; Auto with sets.
+intros X f y H'; elim H'.
+intros x H'0 y0 H'1; rewrite H'1.
+exists x; auto with sets.
 Qed.
 
-Definition injective :=  [f: U -> V] (x, y: U) (f x) == (f y) -> x == y.
+Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.
 
-Lemma not_injective_elim:
-  (f: U -> V) ~ (injective f) ->
-   (EXT x | (EXT y | (f x) == (f y) /\ ~ x == y)).
+Lemma not_injective_elim :
+ forall f:U -> V,
+   ~ injective f ->  exists x : _ | ( exists y : _ | f x = f y /\ x <> y).
 Proof.
-Unfold injective; Intros f H.
-Cut (EXT x | ~ ((y: U) (f x) == (f y) -> x == y)).
-2: Apply not_all_ex_not with P:=[x:U](y: U) (f x) == (f y) -> x == y; 
-   Trivial with sets.
-NewDestruct 1 as [x C]; Exists x.
-Cut (EXT y | ~((f x)==(f y)->x==y)).
-2: Apply not_all_ex_not with P:=[y:U](f x)==(f y)->x==y; Trivial with sets.
-NewDestruct 1 as [y D]; Exists y.
-Apply imply_to_and; Trivial with sets.
+unfold injective in |- *; intros f H.
+cut ( exists x : _ | ~ (forall y:U, f x = f y -> x = y)).
+2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
+    trivial with sets.
+destruct 1 as [x C]; exists x.
+cut ( exists y : _ | ~ (f x = f y -> x = y)).
+2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y);
+    trivial with sets.
+destruct 1 as [y D]; exists y.
+apply imply_to_and; trivial with sets.
 Qed.
 
-Lemma cardinal_Im_intro:
-  (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal ? A n) ->
-   (EX p: nat | (cardinal ? (Im A f) p)).
+Lemma cardinal_Im_intro :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+   cardinal _ A n ->  exists p : nat | cardinal _ (Im A f) p.
 Proof.
-Intros.
-Apply finite_cardinal; Apply finite_image.
-Apply cardinal_finite with n; Trivial with sets.
+intros.
+apply finite_cardinal; apply finite_image.
+apply cardinal_finite with n; trivial with sets.
 Qed.
 
-Lemma In_Image_elim:
-  (A: (Ensemble U)) (f: U -> V) (injective f) ->
-   (x: U) (In ? (Im A f) (f x)) -> (In ? A x).
+Lemma In_Image_elim :
+ forall (A:Ensemble U) (f:U -> V),
+   injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.
 Proof.
-Intros.
-Elim Im_inv with A f (f x); Trivial with sets.
-Intros z C; Elim C; Intros InAz E.
-Elim (H z x E); Trivial with sets.
+intros.
+elim Im_inv with A f (f x); trivial with sets.
+intros z C; elim C; intros InAz E.
+elim (H z x E); trivial with sets.
 Qed.
 
-Lemma injective_preserves_cardinal:
-  (A: (Ensemble U)) (f: U -> V) (n: nat) (injective f) -> (cardinal ? A n) ->
-   (n': nat) (cardinal ? (Im A f) n') -> n' = n.
+Lemma injective_preserves_cardinal :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+   injective f ->
+   cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' = n.
 Proof.
-NewInduction 2 as [|A n H'0 H'1 x H'2]; Auto with sets.
-Rewrite (image_empty f).
-Intros n' CE.
-Apply cardinal_unicity with V (Empty_set V); Auto with sets.
-Intro n'.
-Rewrite (Im_add A x f).
-Intro H'3.
-Elim cardinal_Im_intro with A f n; Trivial with sets.
-Intros i CI.
-LApply (H'1 i); Trivial with sets.
-Cut ~ (In ? (Im A f) (f x)).
-Intros H0 H1.
-Apply cardinal_unicity with V (Add ? (Im A f) (f x)); Trivial with sets.
-Apply card_add; Auto with sets.
-Rewrite <- H1; Trivial with sets.
-Red; Intro; Apply H'2.
-Apply In_Image_elim with f; Trivial with sets.
+induction 2 as [| A n H'0 H'1 x H'2]; auto with sets.
+rewrite (image_empty f).
+intros n' CE.
+apply cardinal_unicity with V (Empty_set V); auto with sets.
+intro n'.
+rewrite (Im_add A x f).
+intro H'3.
+elim cardinal_Im_intro with A f n; trivial with sets.
+intros i CI.
+lapply (H'1 i); trivial with sets.
+cut (~ In _ (Im A f) (f x)).
+intros H0 H1.
+apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets.
+apply card_add; auto with sets.
+rewrite <- H1; trivial with sets.
+red in |- *; intro; apply H'2.
+apply In_Image_elim with f; trivial with sets.
 Qed.
 
-Lemma cardinal_decreases:
-  (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) ->
-   (n': nat) (cardinal V (Im A f) n') -> (le n' n).
+Lemma cardinal_decreases :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+   cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.
 Proof.
-NewInduction 1 as [|A n H'0 H'1 x H'2]; Auto with sets.
-Rewrite (image_empty f); Intros.
-Cut n' = O.
-Intro E; Rewrite E; Trivial with sets.
-Apply cardinal_unicity with V (Empty_set V); Auto with sets.
-Intro n'.
-Rewrite (Im_add A x f).
-Elim cardinal_Im_intro with A f n; Trivial with sets.
-Intros p C H'3.
-Apply le_trans with (S p).
-Apply card_Add_gen with V (Im A f) (f x); Trivial with sets.
-Apply le_n_S; Auto with sets.
+induction 1 as [| A n H'0 H'1 x H'2]; auto with sets.
+rewrite (image_empty f); intros.
+cut (n' = 0).
+intro E; rewrite E; trivial with sets.
+apply cardinal_unicity with V (Empty_set V); auto with sets.
+intro n'.
+rewrite (Im_add A x f).
+elim cardinal_Im_intro with A f n; trivial with sets.
+intros p C H'3.
+apply le_trans with (S p).
+apply card_Add_gen with V (Im A f) (f x); trivial with sets.
+apply le_n_S; auto with sets.
 Qed.
 
-Theorem Pigeonhole:
-  (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) ->
-   (n': nat) (cardinal V (Im A f) n') -> (lt n' n) -> ~ (injective f).
+Theorem Pigeonhole :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+   cardinal U A n ->
+   forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.
 Proof.
-Unfold not; Intros A f n CAn n' CIfn' ltn'n I.
-Cut n' = n.
-Intro E; Generalize ltn'n; Rewrite E; Exact (lt_n_n n).
-Apply injective_preserves_cardinal with A := A f := f n := n; Trivial with sets.
+unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I.
+cut (n' = n).
+intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n).
+apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
+ trivial with sets.
 Qed.
 
-Lemma Pigeonhole_principle:
-  (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal ? A n) ->
-   (n': nat) (cardinal ? (Im A f) n') -> (lt n' n) ->
-    (EXT x | (EXT y | (f x) == (f y) /\ ~ x == y)).
+Lemma Pigeonhole_principle :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+   cardinal _ A n ->
+   forall n':nat,
+     cardinal _ (Im A f) n' ->
+     n' < n ->  exists x : _ | ( exists y : _ | f x = f y /\ x <> y).
 Proof.
-Intros; Apply not_injective_elim.
-Apply Pigeonhole with A n n'; Trivial with sets.
+intros; apply not_injective_elim.
+apply Pigeonhole with A n n'; trivial with sets.
 Qed.
 End Image.
-Hints Resolve Im_def image_empty finite_image : sets v62.
+Hint Resolve Im_def image_empty finite_image: sets v62.
\ No newline at end of file
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index c6233453a..20ec73fa6 100755
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -40,193 +40,205 @@ Require Export Finite_sets_facts.
 Require Export Image.
 
 Section Approx.
-Variable U: Type.
+Variable U : Type.
 
-Inductive Approximant [A, X:(Ensemble U)] : Prop :=
-  Defn_of_Approximant: (Finite U X) -> (Included U X A) -> (Approximant A X).
+Inductive Approximant (A X:Ensemble U) : Prop :=
+    Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X.
 End Approx.
 
-Hints Resolve Defn_of_Approximant.
+Hint Resolve Defn_of_Approximant.
 
 Section Infinite_sets.
-Variable U: Type.
+Variable U : Type.
 
-Lemma make_new_approximant:
-  (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) -> (Approximant U A X) ->
-   (Inhabited U (Setminus U A X)).
+Lemma make_new_approximant :
+ forall A X:Ensemble U,
+   ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).
 Proof.
-Intros A X H' H'0.
-Elim H'0; Intros H'1 H'2.
-Apply Strict_super_set_contains_new_element; Auto with sets.
-Red; Intro H'3; Apply H'.
-Rewrite <- H'3; Auto with sets.
+intros A X H' H'0.
+elim H'0; intros H'1 H'2.
+apply Strict_super_set_contains_new_element; auto with sets.
+red in |- *; intro H'3; apply H'.
+rewrite <- H'3; auto with sets.
 Qed.
 
-Lemma approximants_grow:
-  (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) ->
-   (n: nat) (cardinal U X n) -> (Included U X A) ->
-    (EXT Y | (cardinal U Y (S n)) /\ (Included U Y A)).
+Lemma approximants_grow :
+ forall A X:Ensemble U,
+   ~ Finite U A ->
+   forall n:nat,
+     cardinal U X n ->
+     Included U X A ->  exists Y : _ | cardinal U Y (S n) /\ Included U Y A.
 Proof.
-Intros A X H' n H'0; Elim H'0; Auto with sets.
-Intro H'1.
-Cut (Inhabited U (Setminus U A (Empty_set U))).
-Intro H'2; Elim H'2.
-Intros x H'3.
-Exists (Add U (Empty_set U) x); Auto with sets.
-Split.
-Apply card_add; Auto with sets.
-Cut (In U A x).
-Intro H'4; Red; Auto with sets.
-Intros x0 H'5; Elim H'5; Auto with sets.
-Intros x1 H'6; Elim H'6; Auto with sets.
-Elim H'3; Auto with sets.
-Apply make_new_approximant; Auto with sets.
-Intros A0 n0 H'1 H'2 x H'3 H'5.
-LApply H'2; [Intro H'6; Elim H'6; Clear H'2 | Clear H'2]; Auto with sets.
-Intros x0 H'2; Try Assumption.
-Elim H'2; Intros H'7 H'8; Try Exact H'8; Clear H'2.
-Elim (make_new_approximant A x0); Auto with sets.
-Intros x1 H'2; Try Assumption.
-Exists (Add U x0 x1); Auto with sets.
-Split.
-Apply card_add; Auto with sets.
-Elim H'2; Auto with sets.
-Red.
-Intros x2 H'9; Elim H'9; Auto with sets.
-Intros x3 H'10; Elim H'10; Auto with sets.
-Elim H'2; Auto with sets.
-Auto with sets.
-Apply Defn_of_Approximant; Auto with sets.
-Apply cardinal_finite with n := (S n0); Auto with sets.
+intros A X H' n H'0; elim H'0; auto with sets.
+intro H'1.
+cut (Inhabited U (Setminus U A (Empty_set U))).
+intro H'2; elim H'2.
+intros x H'3.
+exists (Add U (Empty_set U) x); auto with sets.
+split.
+apply card_add; auto with sets.
+cut (In U A x).
+intro H'4; red in |- *; auto with sets.
+intros x0 H'5; elim H'5; auto with sets.
+intros x1 H'6; elim H'6; auto with sets.
+elim H'3; auto with sets.
+apply make_new_approximant; auto with sets.
+intros A0 n0 H'1 H'2 x H'3 H'5.
+lapply H'2; [ intro H'6; elim H'6; clear H'2 | clear H'2 ]; auto with sets.
+intros x0 H'2; try assumption.
+elim H'2; intros H'7 H'8; try exact H'8; clear H'2.
+elim (make_new_approximant A x0); auto with sets.
+intros x1 H'2; try assumption.
+exists (Add U x0 x1); auto with sets.
+split.
+apply card_add; auto with sets.
+elim H'2; auto with sets.
+red in |- *.
+intros x2 H'9; elim H'9; auto with sets.
+intros x3 H'10; elim H'10; auto with sets.
+elim H'2; auto with sets.
+auto with sets.
+apply Defn_of_Approximant; auto with sets.
+apply cardinal_finite with (n := S n0); auto with sets.
 Qed.
 
-Lemma approximants_grow':
-  (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) ->
-   (n: nat) (cardinal U X n) -> (Approximant U A X) ->
-    (EXT Y | (cardinal U Y (S n)) /\ (Approximant U A Y)).
+Lemma approximants_grow' :
+ forall A X:Ensemble U,
+   ~ Finite U A ->
+   forall n:nat,
+     cardinal U X n ->
+     Approximant U A X ->
+      exists Y : _ | cardinal U Y (S n) /\ Approximant U A Y.
 Proof.
-Intros A X H' n H'0 H'1; Try Assumption.
-Elim H'1.
-Intros H'2 H'3.
-ElimType (EXT Y | (cardinal U Y (S n)) /\ (Included U Y A)).
-Intros x H'4; Elim H'4; Intros H'5 H'6; Try Exact H'5; Clear H'4.
-Exists x; Auto with sets.
-Split; [Auto with sets | Idtac].
-Apply Defn_of_Approximant; Auto with sets.
-Apply cardinal_finite with n := (S n); Auto with sets.
-Apply approximants_grow with X := X; Auto with sets.
+intros A X H' n H'0 H'1; try assumption.
+elim H'1.
+intros H'2 H'3.
+elimtype ( exists Y : _ | cardinal U Y (S n) /\ Included U Y A).
+intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
+exists x; auto with sets.
+split; [ auto with sets | idtac ].
+apply Defn_of_Approximant; auto with sets.
+apply cardinal_finite with (n := S n); auto with sets.
+apply approximants_grow with (X := X); auto with sets.
 Qed.
 
-Lemma approximant_can_be_any_size:
-  (A: (Ensemble U)) (X: (Ensemble U)) ~ (Finite U A) ->
-   (n: nat) (EXT Y | (cardinal U Y n) /\ (Approximant U A Y)).
+Lemma approximant_can_be_any_size :
+ forall A X:Ensemble U,
+   ~ Finite U A ->
+   forall n:nat,  exists Y : _ | cardinal U Y n /\ Approximant U A Y.
 Proof.
-Intros A H' H'0 n; Elim n.
-Exists (Empty_set U); Auto with sets.
-Intros n0 H'1; Elim H'1.
-Intros x H'2.
-Apply approximants_grow' with X := x; Tauto.
+intros A H' H'0 n; elim n.
+exists (Empty_set U); auto with sets.
+intros n0 H'1; elim H'1.
+intros x H'2.
+apply approximants_grow' with (X := x); tauto.
 Qed.
 
-Variable V: Type.
+Variable V : Type.
 
-Theorem Image_set_continuous:
-  (A: (Ensemble U))
-  (f: U -> V) (X: (Ensemble V)) (Finite V X) -> (Included V X (Im U V A f)) ->
-   (EX n |
-   (EXT Y | ((cardinal U Y n) /\ (Included U Y A)) /\ (Im U V Y f) == X)).
+Theorem Image_set_continuous :
+ forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
+   Finite V X ->
+   Included V X (Im U V A f) ->
+    exists n : _
+   | ( exists Y : _ | (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
 Proof.
-Intros A f X H'; Elim H'.
-Intro H'0; Exists O.
-Exists (Empty_set U); Auto with sets.
-Intros A0 H'0 H'1 x H'2 H'3; Try Assumption.
-LApply H'1;
- [Intro H'4; Elim H'4; Intros n E; Elim E; Clear H'4 H'1 | Clear H'1]; Auto with sets.
-Intros x0 H'1; Try Assumption.
-Exists (S n); Try Assumption.
-Elim H'1; Intros H'4 H'5; Elim H'4; Intros H'6 H'7; Try Exact H'6; Clear H'4 H'1.
-Clear E.
-Generalize H'2.
-Rewrite <- H'5.
-Intro H'1; Try Assumption.
-Red in H'3.
-Generalize (H'3 x).
-Intro H'4; LApply H'4; [Intro H'8; Try Exact H'8; Clear H'4 | Clear H'4]; Auto with sets.
-Specialize 5 Im_inv with U := U V:=V X := A f := f y := x; Intro H'11; 
- LApply H'11; [Intro H'13; Elim H'11; Clear H'11 | Clear H'11]; Auto with sets.
-Intros x1 H'4; Try Assumption.
-Apply exT_intro with x := (Add U x0 x1).
-Split; [Split; [Try Assumption | Idtac] | Idtac].
-Apply card_add; Auto with sets.
-Red; Intro H'9; Try Exact H'9.
-Apply H'1.
-Elim H'4; Intros H'10 H'11; Rewrite <- H'11; Clear H'4; Auto with sets.
-Elim H'4; Intros H'9 H'10; Try Exact H'9; Clear H'4; Auto with sets.
-Red; Auto with sets.
-Intros x2 H'4; Elim H'4; Auto with sets.
-Intros x3 H'11; Elim H'11; Auto with sets.
-Elim H'4; Intros H'9 H'10; Rewrite <- H'10; Clear H'4; Auto with sets.
-Apply Im_add; Auto with sets.
+intros A f X H'; elim H'.
+intro H'0; exists 0.
+exists (Empty_set U); auto with sets.
+intros A0 H'0 H'1 x H'2 H'3; try assumption.
+lapply H'1;
+ [ intro H'4; elim H'4; intros n E; elim E; clear H'4 H'1 | clear H'1 ];
+ auto with sets.
+intros x0 H'1; try assumption.
+exists (S n); try assumption.
+elim H'1; intros H'4 H'5; elim H'4; intros H'6 H'7; try exact H'6;
+ clear H'4 H'1.
+clear E.
+generalize H'2.
+rewrite <- H'5.
+intro H'1; try assumption.
+red in H'3.
+generalize (H'3 x).
+intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
+ auto with sets.
+specialize  5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
+ intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
+ auto with sets.
+intros x1 H'4; try assumption.
+apply ex_intro with (x := Add U x0 x1).
+split; [ split; [ try assumption | idtac ] | idtac ].
+apply card_add; auto with sets.
+red in |- *; intro H'9; try exact H'9.
+apply H'1.
+elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.
+elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.
+red in |- *; auto with sets.
+intros x2 H'4; elim H'4; auto with sets.
+intros x3 H'11; elim H'11; auto with sets.
+elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.
+apply Im_add; auto with sets.
 Qed.
 
-Theorem Image_set_continuous':
-  (A: (Ensemble U))
-  (f: U -> V) (X: (Ensemble V)) (Approximant V (Im U V A f) X) ->
-   (EXT Y | (Approximant U A Y) /\ (Im U V Y f) == X).
+Theorem Image_set_continuous' :
+ forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
+   Approximant V (Im U V A f) X ->
+    exists Y : _ | Approximant U A Y /\ Im U V Y f = X.
 Proof.
-Intros A f X H'; Try Assumption.
-Cut (EX n | (EXT Y |
-    ((cardinal U Y n) /\ (Included U Y A)) /\ (Im U V Y f) == X)).
-Intro H'0; Elim H'0; Intros n E; Elim E; Clear H'0.
-Intros x H'0; Try Assumption.
-Elim H'0; Intros H'1 H'2; Elim H'1; Intros H'3 H'4; Try Exact H'3;
- Clear H'1 H'0; Auto with sets.
-Exists x.
-Split; [Idtac | Try Assumption].
-Apply Defn_of_Approximant; Auto with sets.
-Apply cardinal_finite with n := n; Auto with sets.
-Apply Image_set_continuous; Auto with sets.
-Elim H'; Auto with sets.
-Elim H'; Auto with sets.
+intros A f X H'; try assumption.
+cut
+ ( exists n : _
+  | ( exists Y : _ | (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).
+intro H'0; elim H'0; intros n E; elim E; clear H'0.
+intros x H'0; try assumption.
+elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3;
+ clear H'1 H'0; auto with sets.
+exists x.
+split; [ idtac | try assumption ].
+apply Defn_of_Approximant; auto with sets.
+apply cardinal_finite with (n := n); auto with sets.
+apply Image_set_continuous; auto with sets.
+elim H'; auto with sets.
+elim H'; auto with sets.
 Qed.
 
-Theorem Pigeonhole_bis:
-  (A: (Ensemble U)) (f: U -> V) ~ (Finite U A) -> (Finite V (Im U V A f)) ->
-   ~ (injective U V f).
+Theorem Pigeonhole_bis :
+ forall (A:Ensemble U) (f:U -> V),
+   ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.
 Proof.
-Intros A f H'0 H'1; Try Assumption.
-Elim (Image_set_continuous' A f (Im U V A f)); Auto with sets.
-Intros x H'2; Elim H'2; Intros H'3 H'4; Try Exact H'3; Clear H'2.
-Elim (make_new_approximant A x); Auto with sets.
-Intros x0 H'2; Elim H'2.
-Intros H'5 H'6.
-Elim (finite_cardinal V (Im U V A f)); Auto with sets.
-Intros n E.
-Elim (finite_cardinal U x); Auto with sets.
-Intros n0 E0.
-Apply Pigeonhole with A := (Add U x x0) n := (S n0) n' := n.
-Apply card_add; Auto with sets.
-Rewrite (Im_add U V x x0 f); Auto with sets.
-Cut (In V (Im U V x f) (f x0)).
-Intro H'8.
-Rewrite (Non_disjoint_union V (Im U V x f) (f x0)); Auto with sets.
-Rewrite H'4; Auto with sets.
-Elim (Extension V (Im U V x f) (Im U V A f)); Auto with sets.
-Apply le_lt_n_Sm.
-Apply cardinal_decreases with U := U V := V A := x f := f; Auto with sets.
-Rewrite H'4; Auto with sets.
-Elim H'3; Auto with sets.
+intros A f H'0 H'1; try assumption.
+elim (Image_set_continuous' A f (Im U V A f)); auto with sets.
+intros x H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
+elim (make_new_approximant A x); auto with sets.
+intros x0 H'2; elim H'2.
+intros H'5 H'6.
+elim (finite_cardinal V (Im U V A f)); auto with sets.
+intros n E.
+elim (finite_cardinal U x); auto with sets.
+intros n0 E0.
+apply Pigeonhole with (A := Add U x x0) (n := S n0) (n' := n).
+apply card_add; auto with sets.
+rewrite (Im_add U V x x0 f); auto with sets.
+cut (In V (Im U V x f) (f x0)).
+intro H'8.
+rewrite (Non_disjoint_union V (Im U V x f) (f x0)); auto with sets.
+rewrite H'4; auto with sets.
+elim (Extension V (Im U V x f) (Im U V A f)); auto with sets.
+apply le_lt_n_Sm.
+apply cardinal_decreases with (U := U) (V := V) (A := x) (f := f);
+ auto with sets.
+rewrite H'4; auto with sets.
+elim H'3; auto with sets.
 Qed.
 
-Theorem Pigeonhole_ter:
-  (A: (Ensemble U))
-  (f: U -> V) (n: nat) (injective U V f) -> (Finite V (Im U V A f)) ->
-   (Finite U A).
+Theorem Pigeonhole_ter :
+ forall (A:Ensemble U) (f:U -> V) (n:nat),
+   injective U V f -> Finite V (Im U V A f) -> Finite U A.
 Proof.
-Intros A f H' H'0 H'1.
-Apply NNPP.
-Red; Intro H'2.
-Elim (Pigeonhole_bis A f); Auto with sets.
+intros A f H' H'0 H'1.
+apply NNPP.
+red in |- *; intro H'2.
+elim (Pigeonhole_bis A f); auto with sets.
 Qed.
 
-End Infinite_sets.
+End Infinite_sets.
\ No newline at end of file
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index dbfc6b463..7f8e1695a 100755
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -46,116 +46,118 @@ Require Export Cpo.
 
 Section Integers_sect.
 
-Inductive Integers : (Ensemble nat) :=
-      Integers_defn: (x: nat) (In nat Integers x).
-Hints Resolve Integers_defn.
+Inductive Integers : Ensemble nat :=
+    Integers_defn : forall x:nat, In nat Integers x.
+Hint Resolve Integers_defn.
 
-Lemma le_reflexive: (Reflexive nat le).
+Lemma le_reflexive : Reflexive nat le.
 Proof.
-Red; Auto with arith.
+red in |- *; auto with arith.
 Qed.
 
-Lemma le_antisym: (Antisymmetric nat le).
+Lemma le_antisym : Antisymmetric nat le.
 Proof.
-Red; Intros x y H H';Rewrite (le_antisym x y);Auto.
+red in |- *; intros x y H H'; rewrite (le_antisym x y); auto.
 Qed.
 
-Lemma le_trans: (Transitive nat le).
+Lemma le_trans : Transitive nat le.
 Proof.
-Red; Intros; Apply le_trans with y;Auto.
+red in |- *; intros; apply le_trans with y; auto.
 Qed.
-Hints Resolve le_reflexive le_antisym le_trans.
+Hint Resolve le_reflexive le_antisym le_trans.
 
-Lemma le_Order: (Order nat le).
+Lemma le_Order : Order nat le.
 Proof.
-Auto with sets arith.
+auto with sets arith.
 Qed.
-Hints Resolve le_Order.
+Hint Resolve le_Order.
 
-Lemma triv_nat: (n: nat) (In nat Integers n).
+Lemma triv_nat : forall n:nat, In nat Integers n.
 Proof.
-Auto with sets arith.
+auto with sets arith.
 Qed.
-Hints Resolve triv_nat.
+Hint Resolve triv_nat.
 
-Definition nat_po: (PO nat).
-Apply Definition_of_PO with Carrier_of := Integers Rel_of := le; Auto with sets arith.
-Apply Inhabited_intro with x := O; Auto with sets arith.
+Definition nat_po : PO nat.
+apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le);
+ auto with sets arith.
+apply Inhabited_intro with (x := 0); auto with sets arith.
 Defined.
-Hints Unfold nat_po.
+Hint Unfold nat_po.
 
-Lemma le_total_order: (Totally_ordered nat nat_po Integers).
+Lemma le_total_order : Totally_ordered nat nat_po Integers.
 Proof.
-Apply Totally_ordered_definition.
-Simpl.
-Intros H' x y H'0.
-Specialize 2 le_or_lt with n := x m := y; Intro H'2; Elim H'2.
-Intro H'1; Left; Auto with sets arith.
-Intro H'1; Right.
-Cut (le y x); Auto with sets arith.
+apply Totally_ordered_definition.
+simpl in |- *.
+intros H' x y H'0.
+specialize  2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
+intro H'1; left; auto with sets arith.
+intro H'1; right.
+cut (y <= x); auto with sets arith.
 Qed.
-Hints Resolve le_total_order.
+Hint Resolve le_total_order.
 
-Lemma Finite_subset_has_lub:
-  (X: (Ensemble nat)) (Finite nat X) ->
-   (EXT m: nat | (Upper_Bound nat nat_po X m)).
+Lemma Finite_subset_has_lub :
+ forall X:Ensemble nat,
+   Finite nat X ->  exists m : nat | Upper_Bound nat nat_po X m.
 Proof.
-Intros X H'; Elim H'.
-Exists O.
-Apply Upper_Bound_definition; Auto with sets arith.
-Intros y H'0; Elim H'0; Auto with sets arith.
-Intros A H'0 H'1 x H'2; Try Assumption.
-Elim H'1; Intros x0 H'3; Clear H'1.
-Elim le_total_order.
-Simpl.
-Intro H'1; Try Assumption.
-LApply H'1; [Intro H'4; Idtac | Try Assumption]; Auto with sets arith.
-Generalize (H'4 x0 x).
-Clear H'4.
-Clear H'1.
-Intro H'1; LApply H'1;
- [Intro H'4; Elim H'4;
-   [Intro H'5; Try Exact H'5; Clear H'4 H'1 | Intro H'5; Clear H'4 H'1] |
-   Clear H'1].
-Exists x.
-Apply Upper_Bound_definition; Auto with sets arith; Simpl.
-Intros y H'1; Elim H'1.
-Generalize le_trans.
-Intro H'4; Red in H'4.
-Intros x1 H'6; Try Assumption.
-Apply H'4 with y := x0; Auto with sets arith.
-Elim H'3; Simpl; Auto with sets arith.
-Intros x1 H'4; Elim H'4; Auto with sets arith.
-Exists x0.
-Apply Upper_Bound_definition; Auto with sets arith; Simpl.
-Intros y H'1; Elim H'1.
-Intros x1 H'4; Try Assumption.
-Elim H'3; Simpl; Auto with sets arith.
-Intros x1 H'4; Elim H'4; Auto with sets arith.
-Red.
-Intros x1 H'1; Elim H'1; Auto with sets arith.
+intros X H'; elim H'.
+exists 0.
+apply Upper_Bound_definition; auto with sets arith.
+intros y H'0; elim H'0; auto with sets arith.
+intros A H'0 H'1 x H'2; try assumption.
+elim H'1; intros x0 H'3; clear H'1.
+elim le_total_order.
+simpl in |- *.
+intro H'1; try assumption.
+lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith.
+generalize (H'4 x0 x).
+clear H'4.
+clear H'1.
+intro H'1; lapply H'1;
+ [ intro H'4; elim H'4;
+    [ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ]
+ | clear H'1 ].
+exists x.
+apply Upper_Bound_definition; auto with sets arith; simpl in |- *.
+intros y H'1; elim H'1.
+generalize le_trans.
+intro H'4; red in H'4.
+intros x1 H'6; try assumption.
+apply H'4 with (y := x0); auto with sets arith.
+elim H'3; simpl in |- *; auto with sets arith.
+intros x1 H'4; elim H'4; auto with sets arith.
+exists x0.
+apply Upper_Bound_definition; auto with sets arith; simpl in |- *.
+intros y H'1; elim H'1.
+intros x1 H'4; try assumption.
+elim H'3; simpl in |- *; auto with sets arith.
+intros x1 H'4; elim H'4; auto with sets arith.
+red in |- *.
+intros x1 H'1; elim H'1; auto with sets arith.
 Qed.
 
-Lemma Integers_has_no_ub: ~ (EXT m:nat | (Upper_Bound nat nat_po Integers m)).
+Lemma Integers_has_no_ub :
+ ~ ( exists m : nat | Upper_Bound nat nat_po Integers m).
 Proof.
-Red; Intro H'; Elim H'.
-Intros x H'0.
-Elim H'0; Intros H'1 H'2.
-Cut (In nat Integers (S x)).
-Intro H'3.
-Specialize 1 H'2 with y := (S x); Intro H'4; LApply H'4;
- [Intro H'5; Clear H'4 | Try Assumption; Clear H'4].
-Simpl in H'5.
-Absurd (le (S x) x); Auto with arith.
-Auto with sets arith.
+red in |- *; intro H'; elim H'.
+intros x H'0.
+elim H'0; intros H'1 H'2.
+cut (In nat Integers (S x)).
+intro H'3.
+specialize  1H'2 with (y := S x); intro H'4; lapply H'4;
+ [ intro H'5; clear H'4 | try assumption; clear H'4 ].
+simpl in H'5.
+absurd (S x <= x); auto with arith.
+auto with sets arith.
 Qed.
 
-Lemma Integers_infinite: ~ (Finite nat Integers).
+Lemma Integers_infinite : ~ Finite nat Integers.
 Proof.
-Generalize Integers_has_no_ub.
-Intro H'; Red; Intro H'0; Try Exact H'0.
-Apply H'.
-Apply Finite_subset_has_lub; Auto with sets arith.
+generalize Integers_has_no_ub.
+intro H'; red in |- *; intro H'0; try exact H'0.
+apply H'.
+apply Finite_subset_has_lub; auto with sets arith.
 Qed.
 
 End Integers_sect.
@@ -163,4 +165,3 @@ End Integers_sect.
 
 
 
-
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 37fb47e27..a3ae98d0a 100755
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -10,7 +10,7 @@
 
 (* G. Huet 1-9-95 *)
 
-Require Permut.
+Require Import Permut.
 
 Set Implicit Arguments.
 
@@ -18,155 +18,159 @@ Section multiset_defs.
 
 Variable A : Set.
 Variable eqA : A -> A -> Prop.
-Hypothesis Aeq_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
+Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
-Inductive multiset : Set := 
-      Bag : (A->nat) -> multiset.
+Inductive multiset : Set :=
+    Bag : (A -> nat) -> multiset.
 
-Definition EmptyBag := (Bag [a:A]O).
-Definition SingletonBag := [a:A]
-	(Bag [a':A]Cases (Aeq_dec a a') of
-                      (left _) => (S O) 
-	           | (right _) => O 
-                   end
-	).
+Definition EmptyBag := Bag (fun a:A => 0).
+Definition SingletonBag (a:A) :=
+  Bag (fun a':A => match Aeq_dec a a' with
+                   | left _ => 1
+                   | right _ => 0
+                   end).
 
-Definition multiplicity : multiset -> A -> nat :=
-  [m:multiset][a:A]let (f) = m in (f a).
+Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a.
 
 (** multiset equality *)
-Definition meq := [m1,m2:multiset]
-    (a:A)(multiplicity m1 a)=(multiplicity m2 a).
+Definition meq (m1 m2:multiset) :=
+  forall a:A, multiplicity m1 a = multiplicity m2 a.
 
-Hints Unfold  meq multiplicity.
+Hint Unfold meq multiplicity.
 
-Lemma meq_refl : (x:multiset)(meq x x).
+Lemma meq_refl : forall x:multiset, meq x x.
 Proof.
-NewDestruct x; Auto.
+destruct x; auto.
 Qed.
-Hints Resolve meq_refl.
+Hint Resolve meq_refl.
 
-Lemma meq_trans : (x,y,z:multiset)(meq x y)->(meq y z)->(meq x z).
+Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.
 Proof.
-Unfold meq.
-NewDestruct x; NewDestruct y; NewDestruct z.
-Intros; Rewrite H; Auto.
+unfold meq in |- *.
+destruct x; destruct y; destruct z.
+intros; rewrite H; auto.
 Qed.
 
-Lemma meq_sym : (x,y:multiset)(meq x y)->(meq y x).
+Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.
 Proof.
-Unfold meq.
-NewDestruct x; NewDestruct y; Auto.
+unfold meq in |- *.
+destruct x; destruct y; auto.
 Qed.
-Hints Immediate meq_sym.
+Hint Immediate meq_sym.
 
 (** multiset union *)
-Definition munion := [m1,m2:multiset]
-    (Bag [a:A](plus (multiplicity m1 a)(multiplicity m2 a))).
+Definition munion (m1 m2:multiset) :=
+  Bag (fun a:A => multiplicity m1 a + multiplicity m2 a).
 
-Lemma munion_empty_left :
-     (x:multiset)(meq x (munion EmptyBag x)).
+Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x).
 Proof.
-Unfold meq; Unfold munion; Simpl; Auto.
+unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
 Qed.
-Hints Resolve munion_empty_left.
+Hint Resolve munion_empty_left.
 
-Lemma munion_empty_right :
-     (x:multiset)(meq x (munion x EmptyBag)).
+Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
 Proof.
-Unfold meq; Unfold munion; Simpl; Auto.
+unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
 Qed.
 
 
-Require Plus. (* comm. and ass. of plus *)
+Require Import Plus. (* comm. and ass. of plus *)
 
-Lemma munion_comm : (x,y:multiset)(meq (munion x y) (munion y x)).
+Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
 Proof.
-Unfold meq; Unfold multiplicity; Unfold munion.
-NewDestruct x; NewDestruct y; Auto with arith.
+unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.
+destruct x; destruct y; auto with arith.
 Qed.
-Hints Resolve munion_comm.
+Hint Resolve munion_comm.
 
-Lemma munion_ass : 
-      (x,y,z:multiset)(meq (munion (munion x y) z) (munion x (munion y z))).
+Lemma munion_ass :
+ forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).
 Proof.
-Unfold meq; Unfold munion; Unfold multiplicity.
-NewDestruct x; NewDestruct y; NewDestruct z; Auto with arith.
+unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+destruct x; destruct y; destruct z; auto with arith.
 Qed.
-Hints Resolve munion_ass.
+Hint Resolve munion_ass.
 
-Lemma meq_left :  (x,y,z:multiset)(meq x y)->(meq (munion x z) (munion y z)).
+Lemma meq_left :
+ forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).
 Proof.
-Unfold meq; Unfold munion; Unfold multiplicity.
-NewDestruct x; NewDestruct y; NewDestruct z.
-Intros; Elim H; Auto with arith.
+unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+destruct x; destruct y; destruct z.
+intros; elim H; auto with arith.
 Qed.
-Hints Resolve meq_left.
+Hint Resolve meq_left.
 
-Lemma meq_right : (x,y,z:multiset)(meq x y)->(meq (munion z x) (munion z y)).
+Lemma meq_right :
+ forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).
 Proof.
-Unfold meq; Unfold munion; Unfold multiplicity.
-NewDestruct x; NewDestruct y; NewDestruct z.
-Intros; Elim H; Auto.
+unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+destruct x; destruct y; destruct z.
+intros; elim H; auto.
 Qed.
-Hints Resolve meq_right.
+Hint Resolve meq_right.
 
 
 (** Here we should make multiset an abstract datatype, by hiding [Bag],
     [munion], [multiplicity]; all further properties are proved abstractly *)
 
 Lemma munion_rotate :
-   (x,y,z:multiset)(meq (munion x (munion y z)) (munion z (munion x y))).
+ forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).
 Proof.
-Intros; Apply (op_rotate multiset munion meq); Auto.
-Exact meq_trans.
+intros; apply (op_rotate multiset munion meq); auto.
+exact meq_trans.
 Qed.
 
-Lemma meq_congr : (x,y,z,t:multiset)(meq x y)->(meq z t)->
-                  (meq (munion x z) (munion y t)).
+Lemma meq_congr :
+ forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).
 Proof.
-Intros; Apply (cong_congr multiset munion meq); Auto.
-Exact meq_trans.
+intros; apply (cong_congr multiset munion meq); auto.
+exact meq_trans.
 Qed.
 
 Lemma munion_perm_left :
-   (x,y,z:multiset)(meq (munion x (munion y z)) (munion y (munion x z))).
+ forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).
 Proof.
-Intros; Apply (perm_left multiset munion meq); Auto.
-Exact meq_trans.
+intros; apply (perm_left multiset munion meq); auto.
+exact meq_trans.
 Qed.
 
-Lemma multiset_twist1 : (x,y,z,t:multiset)
-   (meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z)).
+Lemma multiset_twist1 :
+ forall x y z t:multiset,
+   meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z).
 Proof.
-Intros; Apply (twist multiset munion meq); Auto.
-Exact meq_trans.
+intros; apply (twist multiset munion meq); auto.
+exact meq_trans.
 Qed.
 
-Lemma multiset_twist2 : (x,y,z,t:multiset)
-   (meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t)).
+Lemma multiset_twist2 :
+ forall x y z t:multiset,
+   meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t).
 Proof.
-Intros; Apply meq_trans with (munion (munion x (munion y z)) t).
-Apply meq_sym; Apply munion_ass.
-Apply meq_left; Apply munion_perm_left.
+intros; apply meq_trans with (munion (munion x (munion y z)) t).
+apply meq_sym; apply munion_ass.
+apply meq_left; apply munion_perm_left.
 Qed.
 
 (** specific for treesort *)
 
-Lemma treesort_twist1 : (x,y,z,t,u:multiset) (meq u (munion y z)) ->
-   (meq (munion x (munion u t)) (munion (munion y (munion x t)) z)).
+Lemma treesort_twist1 :
+ forall x y z t u:multiset,
+   meq u (munion y z) ->
+   meq (munion x (munion u t)) (munion (munion y (munion x t)) z).
 Proof.
-Intros; Apply meq_trans with (munion x (munion (munion y z) t)).
-Apply meq_right; Apply meq_left; Trivial.
-Apply multiset_twist1.
+intros; apply meq_trans with (munion x (munion (munion y z) t)).
+apply meq_right; apply meq_left; trivial.
+apply multiset_twist1.
 Qed.
 
-Lemma treesort_twist2 : (x,y,z,t,u:multiset) (meq u (munion y z)) ->
-   (meq (munion x (munion u t)) (munion (munion y (munion x z)) t)).
+Lemma treesort_twist2 :
+ forall x y z t u:multiset,
+   meq u (munion y z) ->
+   meq (munion x (munion u t)) (munion (munion y (munion x z)) t).
 Proof.
-Intros; Apply meq_trans with (munion x (munion (munion y z) t)).
-Apply meq_right; Apply meq_left; Trivial.
-Apply multiset_twist2.
+intros; apply meq_trans with (munion x (munion (munion y z) t)).
+apply meq_right; apply meq_left; trivial.
+apply multiset_twist2.
 Qed.
 
 
@@ -181,6 +185,7 @@ End multiset_defs.
 
 Unset Implicit Arguments.
 
-Hints Unfold meq multiplicity : v62 datatypes.
-Hints Resolve munion_empty_right munion_comm munion_ass meq_left meq_right munion_empty_left : v62 datatypes.
-Hints Immediate meq_sym : v62 datatypes.
+Hint Unfold meq multiplicity: v62 datatypes.
+Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
+  munion_empty_left: v62 datatypes.
+Hint Immediate meq_sym: v62 datatypes.
\ No newline at end of file
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index f3d692b85..5ef6bc9b0 100755
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -30,71 +30,71 @@ Require Export Ensembles.
 Require Export Relations_1.
 
 Section Partial_orders.
-Variable U: Type.
+Variable U : Type.
 
-Definition Carrier :=  (Ensemble U).
+Definition Carrier := Ensemble U.
 
-Definition Rel :=  (Relation U).
+Definition Rel := Relation U.
 
-Record PO : Type := Definition_of_PO {
-   Carrier_of: (Ensemble U);
-   Rel_of: (Relation U);
-   PO_cond1: (Inhabited U Carrier_of);
-   PO_cond2: (Order U Rel_of) }.
-Variable p: PO.
+Record PO : Type := Definition_of_PO
+  {Carrier_of : Ensemble U;
+   Rel_of : Relation U;
+   PO_cond1 : Inhabited U Carrier_of;
+   PO_cond2 : Order U Rel_of}.
+Variable p : PO.
 
-Definition Strict_Rel_of : Rel :=  [x, y: U] (Rel_of p x y) /\ ~ x == y.
+Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y.
 
-Inductive covers [y, x:U]: Prop :=
-      Definition_of_covers:
-      (Strict_Rel_of x y) -> 
-          ~ (EXT z | (Strict_Rel_of x z) /\ (Strict_Rel_of z y)) -> 
-          (covers y x).
+Inductive covers (y x:U) : Prop :=
+    Definition_of_covers :
+      Strict_Rel_of x y ->
+      ~ ( exists z : _ | Strict_Rel_of x z /\ Strict_Rel_of z y) ->
+      covers y x.
 
 End Partial_orders.
 
-Hints Unfold Carrier_of Rel_of  Strict_Rel_of : sets v62.
-Hints Resolve Definition_of_covers : sets v62.
+Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets v62.
+Hint Resolve Definition_of_covers: sets v62.
 
 
 Section Partial_order_facts.
-Variable U:Type.
-Variable D:(PO U).
+Variable U : Type.
+Variable D : PO U.
 
-Lemma Strict_Rel_Transitive_with_Rel:
-  (x:U) (y:U) (z:U) (Strict_Rel_of U D x y) -> (Rel_of U D y z) ->
-  (Strict_Rel_of U D x z).
-Unfold 1 Strict_Rel_of.
-Red.
-Elim D; Simpl.
-Intros C R H' H'0; Elim H'0.
-Intros H'1 H'2 H'3 x y z H'4 H'5; Split.
-Apply H'2 with y := y; Tauto.
-Red; Intro H'6.
-Elim H'4; Intros H'7 H'8; Apply H'8; Clear H'4.
-Apply H'3; Auto.
-Rewrite H'6; Tauto.
+Lemma Strict_Rel_Transitive_with_Rel :
+ forall x y z:U,
+   Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
+unfold Strict_Rel_of at 1 in |- *.
+red in |- *.
+elim D; simpl in |- *.
+intros C R H' H'0; elim H'0.
+intros H'1 H'2 H'3 x y z H'4 H'5; split.
+apply H'2 with (y := y); tauto.
+red in |- *; intro H'6.
+elim H'4; intros H'7 H'8; apply H'8; clear H'4.
+apply H'3; auto.
+rewrite H'6; tauto.
 Qed.
 
-Lemma Strict_Rel_Transitive_with_Rel_left:
-  (x:U) (y:U) (z:U) (Rel_of U D x y) -> (Strict_Rel_of U D y z) ->
-  (Strict_Rel_of U D x z).
-Unfold 1 Strict_Rel_of.
-Red.
-Elim D; Simpl.
-Intros C R H' H'0; Elim H'0.
-Intros H'1 H'2 H'3 x y z H'4 H'5; Split.
-Apply H'2 with y := y; Tauto.
-Red; Intro H'6.
-Elim H'5; Intros H'7 H'8; Apply H'8; Clear H'5.
-Apply H'3; Auto.
-Rewrite <- H'6; Auto.
+Lemma Strict_Rel_Transitive_with_Rel_left :
+ forall x y z:U,
+   Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
+unfold Strict_Rel_of at 1 in |- *.
+red in |- *.
+elim D; simpl in |- *.
+intros C R H' H'0; elim H'0.
+intros H'1 H'2 H'3 x y z H'4 H'5; split.
+apply H'2 with (y := y); tauto.
+red in |- *; intro H'6.
+elim H'5; intros H'7 H'8; apply H'8; clear H'5.
+apply H'3; auto.
+rewrite <- H'6; auto.
 Qed.
 
-Lemma Strict_Rel_Transitive: (Transitive U (Strict_Rel_of U D)).
-Red.
-Intros x y z H' H'0.
-Apply Strict_Rel_Transitive_with_Rel with y := y; 
-  [ Intuition | Unfold Strict_Rel_of in H' H'0; Intuition ].
+Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
+red in |- *.
+intros x y z H' H'0.
+apply Strict_Rel_Transitive_with_Rel with (y := y);
+ [ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
 Qed.
-End Partial_order_facts.
+End Partial_order_facts.
\ No newline at end of file
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 03a8b7428..c3a1da01c 100755
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -15,77 +15,77 @@
 
 Section Axiomatisation.
 
-Variable U: Set.
+Variable U : Set.
 
-Variable op: U -> U -> U.
+Variable op : U -> U -> U.
 
 Variable cong : U -> U -> Prop.
 
-Hypothesis op_comm : (x,y:U)(cong (op x y) (op y x)).
-Hypothesis op_ass  : (x,y,z:U)(cong (op (op x y) z) (op x (op y z))).
+Hypothesis op_comm : forall x y:U, cong (op x y) (op y x).
+Hypothesis op_ass : forall x y z:U, cong (op (op x y) z) (op x (op y z)).
 
-Hypothesis cong_left :  (x,y,z:U)(cong x y)->(cong (op x z) (op y z)).
-Hypothesis cong_right : (x,y,z:U)(cong x y)->(cong (op z x) (op z y)).
-Hypothesis cong_trans : (x,y,z:U)(cong x y)->(cong y z)->(cong x z).
-Hypothesis cong_sym : (x,y:U)(cong x y)->(cong y x).
+Hypothesis cong_left : forall x y z:U, cong x y -> cong (op x z) (op y z).
+Hypothesis cong_right : forall x y z:U, cong x y -> cong (op z x) (op z y).
+Hypothesis cong_trans : forall x y z:U, cong x y -> cong y z -> cong x z.
+Hypothesis cong_sym : forall x y:U, cong x y -> cong y x.
 
 (** Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *)
 
 Lemma cong_congr :
- (x,y,z,t:U)(cong x y)->(cong z t)->(cong (op x z) (op y t)).
+ forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t).
 Proof.
-Intros; Apply cong_trans with (op y z).
-Apply cong_left; Trivial.
-Apply cong_right; Trivial.
+intros; apply cong_trans with (op y z).
+apply cong_left; trivial.
+apply cong_right; trivial.
 Qed.
 
-Lemma comm_right : (x,y,z:U)(cong (op x (op y z)) (op x (op z y))).
+Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)).
 Proof.
-Intros; Apply cong_right; Apply op_comm.
+intros; apply cong_right; apply op_comm.
 Qed.
 
-Lemma comm_left : (x,y,z:U)(cong (op (op x y) z) (op (op y x) z)).
+Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z).
 Proof.
-Intros; Apply cong_left; Apply op_comm.
+intros; apply cong_left; apply op_comm.
 Qed.
 
-Lemma perm_right : (x,y,z:U)(cong (op (op x y) z) (op (op x z) y)).
+Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y).
 Proof.
-Intros.
-Apply cong_trans with (op x (op y z)).
-Apply op_ass.
-Apply cong_trans with (op x (op z y)). 
-Apply cong_right; Apply op_comm.
-Apply cong_sym; Apply op_ass.
+intros.
+apply cong_trans with (op x (op y z)).
+apply op_ass.
+apply cong_trans with (op x (op z y)). 
+apply cong_right; apply op_comm.
+apply cong_sym; apply op_ass.
 Qed.
 
-Lemma perm_left : (x,y,z:U)(cong (op x (op y z)) (op y (op x z))).
+Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)).
 Proof.
-Intros.
-Apply cong_trans with (op (op x y) z).
-Apply cong_sym; Apply op_ass.
-Apply cong_trans with (op (op y x) z).
-Apply cong_left; Apply op_comm.
-Apply op_ass.
+intros.
+apply cong_trans with (op (op x y) z).
+apply cong_sym; apply op_ass.
+apply cong_trans with (op (op y x) z).
+apply cong_left; apply op_comm.
+apply op_ass.
 Qed.
 
-Lemma op_rotate : (x,y,z,t:U)(cong (op x (op y z)) (op z (op x y))).
+Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)).
 Proof.
-Intros; Apply cong_trans with (op (op x y) z).
-Apply cong_sym; Apply op_ass.
-Apply op_comm.
+intros; apply cong_trans with (op (op x y) z).
+apply cong_sym; apply op_ass.
+apply op_comm.
 Qed.
 
 (* Needed for treesort ... *)
-Lemma twist : (x,y,z,t:U)
-   (cong (op x (op (op y z) t)) (op (op y (op x t)) z)).
+Lemma twist :
+ forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z).
 Proof.
-Intros.
-Apply cong_trans with (op x (op (op y t) z)).
-Apply cong_right; Apply perm_right.
-Apply cong_trans with (op (op x (op y t)) z).
-Apply cong_sym; Apply op_ass.
-Apply cong_left; Apply perm_left.
+intros.
+apply cong_trans with (op x (op (op y t) z)).
+apply cong_right; apply perm_right.
+apply cong_trans with (op (op x (op y t)) z).
+apply cong_sym; apply op_ass.
+apply cong_left; apply perm_left.
 Qed.
 
-End Axiomatisation.
+End Axiomatisation.
\ No newline at end of file
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index c9c7188b1..543702276 100755
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -33,156 +33,158 @@ Require Export Partial_Order.
 Require Export Cpo.
 
 Section The_power_set_partial_order.
-Variable U: Type.
+Variable U : Type.
 
-Inductive Power_set [A:(Ensemble U)]: (Ensemble (Ensemble U)) :=
-    Definition_of_Power_set:
-     (X: (Ensemble U)) (Included U X A) -> (In (Ensemble U) (Power_set A) X).
-Hints Resolve Definition_of_Power_set.
+Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
+    Definition_of_Power_set :
+      forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X.
+Hint Resolve Definition_of_Power_set.
 
-Theorem Empty_set_minimal: (X: (Ensemble U)) (Included U (Empty_set U) X).
-Intro X; Red.
-Intros x H'; Elim H'.
+Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X.
+intro X; red in |- *.
+intros x H'; elim H'.
 Qed.
-Hints Resolve Empty_set_minimal.
+Hint Resolve Empty_set_minimal.
 
-Theorem Power_set_Inhabited:
-  (X: (Ensemble U)) (Inhabited (Ensemble U) (Power_set X)).
-Intro X.
-Apply Inhabited_intro with (Empty_set U); Auto with sets.
+Theorem Power_set_Inhabited :
+ forall X:Ensemble U, Inhabited (Ensemble U) (Power_set X).
+intro X.
+apply Inhabited_intro with (Empty_set U); auto with sets.
 Qed.
-Hints Resolve Power_set_Inhabited.
+Hint Resolve Power_set_Inhabited.
 
-Theorem Inclusion_is_an_order: (Order (Ensemble U) (Included U)).
-Auto 6 with sets.
+Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U).
+auto 6 with sets.
 Qed.
-Hints Resolve Inclusion_is_an_order.
+Hint Resolve Inclusion_is_an_order.
 
-Theorem Inclusion_is_transitive: (Transitive (Ensemble U) (Included U)).
-Elim Inclusion_is_an_order; Auto with sets.
+Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U).
+elim Inclusion_is_an_order; auto with sets.
 Qed.
-Hints Resolve Inclusion_is_transitive.
+Hint Resolve Inclusion_is_transitive.
 
-Definition Power_set_PO: (Ensemble U) -> (PO (Ensemble U)).
-Intro A; Try Assumption.
-Apply Definition_of_PO with (Power_set A) (Included U); Auto with sets.
+Definition Power_set_PO : Ensemble U -> PO (Ensemble U).
+intro A; try assumption.
+apply Definition_of_PO with (Power_set A) (Included U); auto with sets.
 Defined.
-Hints Unfold  Power_set_PO.
+Hint Unfold Power_set_PO.
 
-Theorem Strict_Rel_is_Strict_Included:
-  (same_relation
-     (Ensemble U) (Strict_Included U)
-     (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U)))).
-Auto with sets.
+Theorem Strict_Rel_is_Strict_Included :
+ same_relation (Ensemble U) (Strict_Included U)
+   (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))).
+auto with sets.
 Qed.
-Hints Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included.
+Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included.
 
-Lemma Strict_inclusion_is_transitive_with_inclusion:
-  (x, y, z:(Ensemble U)) (Strict_Included U x y) -> (Included U y z) ->
-  (Strict_Included U x z).
-Intros x y z H' H'0; Try Assumption.
-Elim Strict_Rel_is_Strict_Included.
-Unfold contains.
-Intros H'1 H'2; Try Assumption.
-Apply H'1.
-Apply Strict_Rel_Transitive_with_Rel with y := y; Auto with sets.
+Lemma Strict_inclusion_is_transitive_with_inclusion :
+ forall x y z:Ensemble U,
+   Strict_Included U x y -> Included U y z -> Strict_Included U x z.
+intros x y z H' H'0; try assumption.
+elim Strict_Rel_is_Strict_Included.
+unfold contains in |- *.
+intros H'1 H'2; try assumption.
+apply H'1.
+apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets.
 Qed.
 
-Lemma Strict_inclusion_is_transitive_with_inclusion_left:
-  (x, y, z:(Ensemble U)) (Included U x y) -> (Strict_Included U y z) ->
-  (Strict_Included U x z).
-Intros x y z H' H'0; Try Assumption.
-Elim Strict_Rel_is_Strict_Included.
-Unfold contains.
-Intros H'1 H'2; Try Assumption.
-Apply H'1.
-Apply Strict_Rel_Transitive_with_Rel_left with y := y; Auto with sets.
+Lemma Strict_inclusion_is_transitive_with_inclusion_left :
+ forall x y z:Ensemble U,
+   Included U x y -> Strict_Included U y z -> Strict_Included U x z.
+intros x y z H' H'0; try assumption.
+elim Strict_Rel_is_Strict_Included.
+unfold contains in |- *.
+intros H'1 H'2; try assumption.
+apply H'1.
+apply Strict_Rel_Transitive_with_Rel_left with (y := y); auto with sets.
 Qed.
 
-Lemma Strict_inclusion_is_transitive:
-  (Transitive (Ensemble U) (Strict_Included U)).
-Apply cong_transitive_same_relation
-     with R := (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))); Auto with sets.
+Lemma Strict_inclusion_is_transitive :
+ Transitive (Ensemble U) (Strict_Included U).
+apply cong_transitive_same_relation with
+ (R := Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U)));
+ auto with sets.
 Qed.
 
-Theorem Empty_set_is_Bottom:
-  (A: (Ensemble U)) (Bottom (Ensemble U) (Power_set_PO A) (Empty_set U)).
-Intro A; Apply Bottom_definition; Simpl; Auto with sets.
+Theorem Empty_set_is_Bottom :
+ forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
+intro A; apply Bottom_definition; simpl in |- *; auto with sets.
 Qed.
-Hints Resolve Empty_set_is_Bottom.
+Hint Resolve Empty_set_is_Bottom.
 
-Theorem Union_minimal:
-  (a, b, X: (Ensemble U)) (Included U a X) -> (Included U b X) ->
-   (Included U (Union U a b) X).
-Intros a b X H' H'0; Red.
-Intros x H'1; Elim H'1; Auto with sets.
+Theorem Union_minimal :
+ forall a b X:Ensemble U,
+   Included U a X -> Included U b X -> Included U (Union U a b) X.
+intros a b X H' H'0; red in |- *.
+intros x H'1; elim H'1; auto with sets.
 Qed.
-Hints Resolve Union_minimal.
+Hint Resolve Union_minimal.
 
-Theorem Intersection_maximal:
-  (a, b, X: (Ensemble U)) (Included U X a) -> (Included U X b) ->
-   (Included U X (Intersection U a b)).
-Auto with sets.
+Theorem Intersection_maximal :
+ forall a b X:Ensemble U,
+   Included U X a -> Included U X b -> Included U X (Intersection U a b).
+auto with sets.
 Qed.
 
-Theorem Union_increases_l: (a, b: (Ensemble U)) (Included U a (Union U a b)).
-Auto with sets.
+Theorem Union_increases_l : forall a b:Ensemble U, Included U a (Union U a b).
+auto with sets.
 Qed.
 
-Theorem Union_increases_r: (a, b: (Ensemble U)) (Included U b (Union U a b)).
-Auto with sets.
+Theorem Union_increases_r : forall a b:Ensemble U, Included U b (Union U a b).
+auto with sets.
 Qed.
 
-Theorem Intersection_decreases_l:
-  (a, b: (Ensemble U)) (Included U (Intersection U a b) a).
-Intros a b; Red.
-Intros x H'; Elim H'; Auto with sets.
+Theorem Intersection_decreases_l :
+ forall a b:Ensemble U, Included U (Intersection U a b) a.
+intros a b; red in |- *.
+intros x H'; elim H'; auto with sets.
 Qed.
 
-Theorem Intersection_decreases_r:
-  (a, b: (Ensemble U)) (Included U (Intersection U a b) b).
-Intros a b; Red.
-Intros x H'; Elim H'; Auto with sets.
+Theorem Intersection_decreases_r :
+ forall a b:Ensemble U, Included U (Intersection U a b) b.
+intros a b; red in |- *.
+intros x H'; elim H'; auto with sets.
 Qed.
-Hints Resolve Union_increases_l Union_increases_r Intersection_decreases_l
-     Intersection_decreases_r.
+Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
+  Intersection_decreases_r.
 
-Theorem Union_is_Lub:
-  (A: (Ensemble U)) (a, b: (Ensemble U)) (Included U a A) -> (Included U b A) ->
-   (Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b)).
-Intros A a b H' H'0.
-Apply Lub_definition; Simpl.
-Apply Upper_Bound_definition; Simpl; Auto with sets.
-Intros y H'1; Elim H'1; Auto with sets.
-Intros y H'1; Elim H'1; Simpl; Auto with sets.
+Theorem Union_is_Lub :
+ forall A a b:Ensemble U,
+   Included U a A ->
+   Included U b A ->
+   Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b).
+intros A a b H' H'0.
+apply Lub_definition; simpl in |- *.
+apply Upper_Bound_definition; simpl in |- *; auto with sets.
+intros y H'1; elim H'1; auto with sets.
+intros y H'1; elim H'1; simpl in |- *; auto with sets.
 Qed.
 
-Theorem Intersection_is_Glb:
-  (A: (Ensemble U)) (a, b: (Ensemble U)) (Included U a A) -> (Included U b A) ->
-   (Glb
-      (Ensemble U)
-      (Power_set_PO A)
-      (Couple (Ensemble U) a b)
-      (Intersection U a b)).
-Intros A a b H' H'0.
-Apply Glb_definition; Simpl.
-Apply Lower_Bound_definition; Simpl; Auto with sets.
-Apply Definition_of_Power_set.
-Generalize Inclusion_is_transitive; Intro IT; Red in IT; Apply IT with a; Auto with sets.
-Intros y H'1; Elim H'1; Auto with sets.
-Intros y H'1; Elim H'1; Simpl; Auto with sets.
+Theorem Intersection_is_Glb :
+ forall A a b:Ensemble U,
+   Included U a A ->
+   Included U b A ->
+   Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b)
+     (Intersection U a b).
+intros A a b H' H'0.
+apply Glb_definition; simpl in |- *.
+apply Lower_Bound_definition; simpl in |- *; auto with sets.
+apply Definition_of_Power_set.
+generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a;
+ auto with sets.
+intros y H'1; elim H'1; auto with sets.
+intros y H'1; elim H'1; simpl in |- *; auto with sets.
 Qed.
 
 End The_power_set_partial_order.
 
-Hints Resolve Empty_set_minimal : sets v62.
-Hints Resolve Power_set_Inhabited : sets v62.
-Hints Resolve Inclusion_is_an_order : sets v62.
-Hints Resolve Inclusion_is_transitive : sets v62.
-Hints Resolve Union_minimal : sets v62.
-Hints Resolve Union_increases_l : sets v62.
-Hints Resolve Union_increases_r : sets v62.
-Hints Resolve Intersection_decreases_l : sets v62.
-Hints Resolve Intersection_decreases_r : sets v62.
-Hints Resolve Empty_set_is_Bottom : sets v62.
-Hints Resolve Strict_inclusion_is_transitive : sets v62.
+Hint Resolve Empty_set_minimal: sets v62.
+Hint Resolve Power_set_Inhabited: sets v62.
+Hint Resolve Inclusion_is_an_order: sets v62.
+Hint Resolve Inclusion_is_transitive: sets v62.
+Hint Resolve Union_minimal: sets v62.
+Hint Resolve Union_increases_l: sets v62.
+Hint Resolve Union_increases_r: sets v62.
+Hint Resolve Intersection_decreases_l: sets v62.
+Hint Resolve Intersection_decreases_r: sets v62.
+Hint Resolve Empty_set_is_Bottom: sets v62.
+Hint Resolve Strict_inclusion_is_transitive: sets v62.
\ No newline at end of file
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 6b3443b7d..988bbd25a 100755
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -39,300 +39,304 @@ Require Export Classical_sets.
 
 Section Sets_as_an_algebra.
 
-Variable U: Type.
+Variable U : Type.
 
-Lemma sincl_add_x:
-  (A, B: (Ensemble U))
-  (x: U) ~ (In U A x) -> (Strict_Included U (Add U A x) (Add U B x)) ->
-                         (Strict_Included U A B).
+Lemma sincl_add_x :
+ forall (A B:Ensemble U) (x:U),
+   ~ In U A x ->
+   Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
 Proof.
-Intros A B x H' H'0; Red.
-LApply (Strict_Included_inv U (Add U A x) (Add U B x)); Auto with sets.
-Clear H'0; Intro H'0; Split.
-Apply incl_add_x with x := x; Tauto.
-Elim H'0; Intros H'1 H'2; Elim H'2; Clear H'0 H'2.
-Intros x0 H'0.
-Red; Intro H'2.
-Elim H'0; Clear H'0.
-Rewrite <- H'2; Auto with sets.
+intros A B x H' H'0; red in |- *.
+lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.
+clear H'0; intro H'0; split.
+apply incl_add_x with (x := x); tauto.
+elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.
+intros x0 H'0.
+red in |- *; intro H'2.
+elim H'0; clear H'0.
+rewrite <- H'2; auto with sets.
 Qed.
 
-Lemma incl_soustr_in:
-  (X: (Ensemble U)) (x: U) (In U X x) -> (Included U (Subtract U X x) X).
+Lemma incl_soustr_in :
+ forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.
 Proof.
-Intros X x H'; Red.
-Intros x0 H'0; Elim H'0; Auto with sets.
+intros X x H'; red in |- *.
+intros x0 H'0; elim H'0; auto with sets.
 Qed.
-Hints Resolve incl_soustr_in : sets v62.
+Hint Resolve incl_soustr_in: sets v62.
 
-Lemma incl_soustr:
-  (X, Y: (Ensemble U)) (x: U) (Included U X Y) ->
-   (Included U (Subtract U X x) (Subtract U Y x)).
+Lemma incl_soustr :
+ forall (X Y:Ensemble U) (x:U),
+   Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
 Proof.
-Intros X Y x H'; Red.
-Intros x0 H'0; Elim H'0.
-Intros H'1 H'2.
-Apply Subtract_intro; Auto with sets.
+intros X Y x H'; red in |- *.
+intros x0 H'0; elim H'0.
+intros H'1 H'2.
+apply Subtract_intro; auto with sets.
 Qed.
-Hints Resolve incl_soustr : sets v62.
+Hint Resolve incl_soustr: sets v62.
 
 
-Lemma incl_soustr_add_l:
-  (X: (Ensemble U)) (x: U) (Included U (Subtract U (Add U X x) x) X).
+Lemma incl_soustr_add_l :
+ forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
 Proof.
-Intros X x; Red.
-Intros x0 H'; Elim H'; Auto with sets.
-Intro H'0; Elim H'0; Auto with sets.
-Intros t H'1 H'2; Elim H'2; Auto with sets.
+intros X x; red in |- *.
+intros x0 H'; elim H'; auto with sets.
+intro H'0; elim H'0; auto with sets.
+intros t H'1 H'2; elim H'2; auto with sets.
 Qed.
-Hints Resolve incl_soustr_add_l : sets v62.
+Hint Resolve incl_soustr_add_l: sets v62.
 
-Lemma incl_soustr_add_r:
-  (X: (Ensemble U)) (x: U) ~ (In U X x) ->
-   (Included U X (Subtract U (Add U X x) x)).
+Lemma incl_soustr_add_r :
+ forall (X:Ensemble U) (x:U),
+   ~ In U X x -> Included U X (Subtract U (Add U X x) x).
 Proof.
-Intros X x H'; Red.
-Intros x0 H'0; Try Assumption.
-Apply Subtract_intro; Auto with sets.
-Red; Intro H'1; Apply H'; Rewrite H'1; Auto with sets.
+intros X x H'; red in |- *.
+intros x0 H'0; try assumption.
+apply Subtract_intro; auto with sets.
+red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
 Qed.
-Hints Resolve incl_soustr_add_r : sets v62.
+Hint Resolve incl_soustr_add_r: sets v62.
 
-Lemma add_soustr_2:
-  (X: (Ensemble U)) (x: U) (In U X x) ->
-   (Included U X (Add U (Subtract U X x) x)).
+Lemma add_soustr_2 :
+ forall (X:Ensemble U) (x:U),
+   In U X x -> Included U X (Add U (Subtract U X x) x).
 Proof.
-Intros X x H'; Red.
-Intros x0 H'0; Try Assumption.
-Elim (classic x == x0); Intro K; Auto with sets.
-Elim K; Auto with sets.
+intros X x H'; red in |- *.
+intros x0 H'0; try assumption.
+elim (classic (x = x0)); intro K; auto with sets.
+elim K; auto with sets.
 Qed.
 
-Lemma add_soustr_1:
-  (X: (Ensemble U)) (x: U) (In U X x) ->
-   (Included U (Add U (Subtract U X x) x) X).
+Lemma add_soustr_1 :
+ forall (X:Ensemble U) (x:U),
+   In U X x -> Included U (Add U (Subtract U X x) x) X.
 Proof.
-Intros X x H'; Red.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intros y H'1; Elim H'1; Auto with sets.
-Intros t H'1; Try Assumption.
-Rewrite <- (Singleton_inv U x t); Auto with sets.
+intros X x H'; red in |- *.
+intros x0 H'0; elim H'0; auto with sets.
+intros y H'1; elim H'1; auto with sets.
+intros t H'1; try assumption.
+rewrite <- (Singleton_inv U x t); auto with sets.
 Qed.
-Hints Resolve add_soustr_1 add_soustr_2 : sets v62.
+Hint Resolve add_soustr_1 add_soustr_2: sets v62.
 
-Lemma add_soustr_xy:
-  (X: (Ensemble U)) (x, y: U) ~ x == y ->
-    (Subtract U (Add U X x) y) == (Add U (Subtract U X y) x).
+Lemma add_soustr_xy :
+ forall (X:Ensemble U) (x y:U),
+   x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
 Proof.
-Intros X x y H'; Apply Extensionality_Ensembles.
-Split; Red.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intro H'1; Elim H'1.
-Intros u H'2 H'3; Try Assumption.
-Apply Add_intro1.
-Apply Subtract_intro; Auto with sets.
-Intros t H'2 H'3; Try Assumption.
-Elim (Singleton_inv U x t); Auto with sets.
-Intros u H'2; Try Assumption.
-Elim (Add_inv U (Subtract U X y) x u); Auto with sets.
-Intro H'0; Elim H'0; Auto with sets.
-Intro H'0; Rewrite <- H'0; Auto with sets.
+intros X x y H'; apply Extensionality_Ensembles.
+split; red in |- *.
+intros x0 H'0; elim H'0; auto with sets.
+intro H'1; elim H'1.
+intros u H'2 H'3; try assumption.
+apply Add_intro1.
+apply Subtract_intro; auto with sets.
+intros t H'2 H'3; try assumption.
+elim (Singleton_inv U x t); auto with sets.
+intros u H'2; try assumption.
+elim (Add_inv U (Subtract U X y) x u); auto with sets.
+intro H'0; elim H'0; auto with sets.
+intro H'0; rewrite <- H'0; auto with sets.
 Qed.
-Hints Resolve add_soustr_xy : sets v62.
+Hint Resolve add_soustr_xy: sets v62.
 
-Lemma incl_st_add_soustr:
-  (X, Y: (Ensemble U)) (x: U) ~ (In U X x) -> 
-   (Strict_Included U (Add U X x) Y) ->
-   (Strict_Included U X (Subtract U Y x)).
+Lemma incl_st_add_soustr :
+ forall (X Y:Ensemble U) (x:U),
+   ~ In U X x ->
+   Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).
 Proof.
-Intros X Y x H' H'0; Apply sincl_add_x with x := x; Auto with sets.
-Split.
-Elim H'0.
-Intros H'1 H'2.
-Generalize (Inclusion_is_transitive U).
-Intro H'4; Red in H'4.
-Apply H'4 with y := Y; Auto with sets.
-Red in H'0.
-Elim H'0; Intros H'1 H'2; Try Exact H'1; Clear H'0. (* PB *)
-Red; Intro H'0; Apply H'2.
-Rewrite H'0; Auto 8 with sets.
+intros X Y x H' H'0; apply sincl_add_x with (x := x); auto with sets.
+split.
+elim H'0.
+intros H'1 H'2.
+generalize (Inclusion_is_transitive U).
+intro H'4; red in H'4.
+apply H'4 with (y := Y); auto with sets.
+red in H'0.
+elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)
+red in |- *; intro H'0; apply H'2.
+rewrite H'0; auto 8 with sets.
 Qed.
 
-Lemma Sub_Add_new:
-  (X: (Ensemble U)) (x: U) ~ (In U X x) -> X == (Subtract U (Add U X x) x).
+Lemma Sub_Add_new :
+ forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
 
-Lemma Simplify_add:
-  (X, X0 : (Ensemble U)) (x: U)
-  ~ (In U X x) -> ~ (In U X0 x) ->  (Add U X x) == (Add U X0 x) -> X == X0.
+Lemma Simplify_add :
+ forall (X X0:Ensemble U) (x:U),
+   ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
 Proof.
-Intros X X0 x H' H'0 H'1; Try Assumption.
-Rewrite (Sub_Add_new X x); Auto with sets.
-Rewrite (Sub_Add_new X0 x); Auto with sets.
-Rewrite H'1; Auto with sets.
+intros X X0 x H' H'0 H'1; try assumption.
+rewrite (Sub_Add_new X x); auto with sets.
+rewrite (Sub_Add_new X0 x); auto with sets.
+rewrite H'1; auto with sets.
 Qed.
 
-Lemma Included_Add:
-  (X, A: (Ensemble U)) (x: U) (Included U X (Add U A x)) ->
-   (Included U X A) \/
-   (EXT A' | X == (Add U A' x) /\ (Included U A' A)).
+Lemma Included_Add :
+ forall (X A:Ensemble U) (x:U),
+   Included U X (Add U A x) ->
+   Included U X A \/ ( exists A' : _ | X = Add U A' x /\ Included U A' A).
 Proof.
-Intros X A x H'0; Try Assumption.
-Elim (classic (In U X x)).
-Intro H'1; Right; Try Assumption.
-Exists (Subtract U X x).
-Split; Auto with sets.
-Red in H'0.
-Red.
-Intros x0 H'2; Try Assumption.
-LApply (Subtract_inv U X x x0); Auto with sets.
-Intro H'3; Elim H'3; Intros K K'; Clear H'3.
-LApply (H'0 x0); Auto with sets.
-Intro H'3; Try Assumption.
-LApply (Add_inv U A x x0); Auto with sets.
-Intro H'4; Elim H'4;
- [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4].
-Elim K'; Auto with sets.
-Intro H'1; Left; Try Assumption.
-Red in H'0.
-Red.
-Intros x0 H'2; Try Assumption.
-LApply (H'0 x0); Auto with sets.
-Intro H'3; Try Assumption.
-LApply (Add_inv U A x x0); Auto with sets.
-Intro H'4; Elim H'4;
- [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4].
-Absurd (In U X x0); Auto with sets.
-Rewrite <- H'5; Auto with sets.
+intros X A x H'0; try assumption.
+elim (classic (In U X x)).
+intro H'1; right; try assumption.
+exists (Subtract U X x).
+split; auto with sets.
+red in H'0.
+red in |- *.
+intros x0 H'2; try assumption.
+lapply (Subtract_inv U X x x0); auto with sets.
+intro H'3; elim H'3; intros K K'; clear H'3.
+lapply (H'0 x0); auto with sets.
+intro H'3; try assumption.
+lapply (Add_inv U A x x0); auto with sets.
+intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+elim K'; auto with sets.
+intro H'1; left; try assumption.
+red in H'0.
+red in |- *.
+intros x0 H'2; try assumption.
+lapply (H'0 x0); auto with sets.
+intro H'3; try assumption.
+lapply (Add_inv U A x x0); auto with sets.
+intro H'4; elim H'4;
+ [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
+absurd (In U X x0); auto with sets.
+rewrite <- H'5; auto with sets.
 Qed.
 
-Lemma setcover_inv:
- (A: (Ensemble U))
- (x, y: (Ensemble U)) (covers (Ensemble U) (Power_set_PO U A) y x) ->
- (Strict_Included U x y) /\
- ((z: (Ensemble U)) (Included U x z) -> (Included U z y) -> x == z \/ z == y).
+Lemma setcover_inv :
+ forall A x y:Ensemble U,
+   covers (Ensemble U) (Power_set_PO U A) y x ->
+   Strict_Included U x y /\
+   (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
 Proof.
-Intros A x y H'; Elim H'.
-Unfold Strict_Rel_of; Simpl.
-Intros H'0 H'1; Split; [Auto with sets | Idtac].
-Intros z H'2 H'3; Try Assumption.
-Elim (classic  x == z); Auto with sets.
-Intro H'4; Right; Try Assumption.
-Elim (classic  z == y); Auto with sets.
-Intro H'5; Try Assumption.
-Elim H'1.
-Exists z; Auto with sets.
+intros A x y H'; elim H'.
+unfold Strict_Rel_of in |- *; simpl in |- *.
+intros H'0 H'1; split; [ auto with sets | idtac ].
+intros z H'2 H'3; try assumption.
+elim (classic (x = z)); auto with sets.
+intro H'4; right; try assumption.
+elim (classic (z = y)); auto with sets.
+intro H'5; try assumption.
+elim H'1.
+exists z; auto with sets.
 Qed.
 
-Theorem Add_covers:
-  (A: (Ensemble U)) (a: (Ensemble U)) (Included U a A) ->
-   (x: U) (In U A x) -> ~ (In U a x) ->
-    (covers (Ensemble U) (Power_set_PO U A) (Add U a x) a).
+Theorem Add_covers :
+ forall A a:Ensemble U,
+   Included U a A ->
+   forall x:U,
+     In U A x ->
+     ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.
 Proof.
-Intros A a H' x H'0 H'1; Try Assumption.
-Apply setcover_intro; Auto with sets.
-Red.
-Split; [Idtac | Red; Intro H'2; Try Exact H'2]; Auto with sets.
-Apply H'1.
-Rewrite H'2; Auto with sets.
-Red; Intro H'2; Elim H'2; Clear H'2.
-Intros z H'2; Elim H'2; Intros H'3 H'4; Try Exact H'3; Clear H'2.
-LApply (Strict_Included_inv U a z); Auto with sets; Clear H'3.
-Intro H'2; Elim H'2; Intros H'3 H'5; Elim H'5; Clear H'2 H'5.
-Intros x0 H'2; Elim H'2.
-Intros H'5 H'6; Try Assumption.
-Generalize H'4; Intro K.
-Red in H'4.
-Elim H'4; Intros H'8 H'9; Red in H'8; Clear H'4.
-LApply (H'8 x0); Auto with sets.
-Intro H'7; Try Assumption.
-Elim (Add_inv U a x x0); Auto with sets.
-Intro H'15.
-Cut (Included U (Add U a x) z).
-Intro H'10; Try Assumption.
-Red in K.
-Elim K; Intros H'11 H'12; Apply H'12; Clear K; Auto with sets.
-Rewrite H'15.
-Red.
-Intros x1 H'10; Elim H'10; Auto with sets.
-Intros x2 H'11; Elim H'11; Auto with sets.
+intros A a H' x H'0 H'1; try assumption.
+apply setcover_intro; auto with sets.
+red in |- *.
+split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets.
+apply H'1.
+rewrite H'2; auto with sets.
+red in |- *; intro H'2; elim H'2; clear H'2.
+intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
+lapply (Strict_Included_inv U a z); auto with sets; clear H'3.
+intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.
+intros x0 H'2; elim H'2.
+intros H'5 H'6; try assumption.
+generalize H'4; intro K.
+red in H'4.
+elim H'4; intros H'8 H'9; red in H'8; clear H'4.
+lapply (H'8 x0); auto with sets.
+intro H'7; try assumption.
+elim (Add_inv U a x x0); auto with sets.
+intro H'15.
+cut (Included U (Add U a x) z).
+intro H'10; try assumption.
+red in K.
+elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.
+rewrite H'15.
+red in |- *.
+intros x1 H'10; elim H'10; auto with sets.
+intros x2 H'11; elim H'11; auto with sets.
 Qed.
 
-Theorem covers_Add:
-  (A: (Ensemble U))
-  (a, a': (Ensemble U))
-  (Included U a A) ->
-  (Included U a' A) -> (covers (Ensemble U) (Power_set_PO U A) a' a) ->
-   (EXT x | a' == (Add U a x) /\ ((In U A x) /\ ~ (In U a x))).
+Theorem covers_Add :
+ forall A a a':Ensemble U,
+   Included U a A ->
+   Included U a' A ->
+   covers (Ensemble U) (Power_set_PO U A) a' a ->
+    exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x.
 Proof.
-Intros A a a' H' H'0 H'1; Try Assumption.
-Elim (setcover_inv A a a'); Auto with sets.
-Intros H'6 H'7.
-Clear H'1.
-Elim (Strict_Included_inv U a a'); Auto with sets.
-Intros H'5 H'8; Elim H'8.
-Intros x H'1; Elim H'1.
-Intros H'2 H'3; Try Assumption.
-Exists x.
-Split; [Try Assumption | Idtac].
-Clear H'8 H'1.
-Elim (H'7 (Add U a x)); Auto with sets.
-Intro H'1.
-Absurd a ==(Add U a x); Auto with sets.
-Red; Intro H'8; Try Exact H'8.
-Apply H'3.
-Rewrite H'8; Auto with sets.
-Auto with sets.
-Red.
-Intros x0 H'1; Elim H'1; Auto with sets.
-Intros x1 H'8; Elim H'8; Auto with sets.
-Split; [Idtac | Try Assumption].
-Red in H'0; Auto with sets.
+intros A a a' H' H'0 H'1; try assumption.
+elim (setcover_inv A a a'); auto with sets.
+intros H'6 H'7.
+clear H'1.
+elim (Strict_Included_inv U a a'); auto with sets.
+intros H'5 H'8; elim H'8.
+intros x H'1; elim H'1.
+intros H'2 H'3; try assumption.
+exists x.
+split; [ try assumption | idtac ].
+clear H'8 H'1.
+elim (H'7 (Add U a x)); auto with sets.
+intro H'1.
+absurd (a = Add U a x); auto with sets.
+red in |- *; intro H'8; try exact H'8.
+apply H'3.
+rewrite H'8; auto with sets.
+auto with sets.
+red in |- *.
+intros x0 H'1; elim H'1; auto with sets.
+intros x1 H'8; elim H'8; auto with sets.
+split; [ idtac | try assumption ].
+red in H'0; auto with sets.
 Qed.
 
-Theorem covers_is_Add:
-  (A: (Ensemble U))
-  (a, a': (Ensemble U)) (Included U a A) -> (Included U a' A) ->
-   (iff
-      (covers (Ensemble U) (Power_set_PO U A) a' a)
-      (EXT x | a' == (Add U a x) /\ ((In U A x) /\ ~ (In U a x)))).
+Theorem covers_is_Add :
+ forall A a a':Ensemble U,
+   Included U a A ->
+   Included U a' A ->
+   (covers (Ensemble U) (Power_set_PO U A) a' a <->
+    ( exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x)).
 Proof.
-Intros A a a' H' H'0; Split; Intro K.
-Apply covers_Add with A := A; Auto with sets.
-Elim K.
-Intros x H'1; Elim H'1; Intros H'2 H'3; Rewrite H'2; Clear H'1.
-Apply Add_covers; Intuition.
+intros A a a' H' H'0; split; intro K.
+apply covers_Add with (A := A); auto with sets.
+elim K.
+intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.
+apply Add_covers; intuition.
 Qed.
 
-Theorem Singleton_atomic:
-  (x:U) (A:(Ensemble U)) (In U A x) ->
-  (covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U)).
-Intros x A H'.
-Rewrite <- (Empty_set_zero' U x).
-Apply Add_covers; Auto with sets.
+Theorem Singleton_atomic :
+ forall (x:U) (A:Ensemble U),
+   In U A x ->
+   covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U).
+intros x A H'.
+rewrite <- (Empty_set_zero' U x).
+apply Add_covers; auto with sets.
 Qed.
 
-Lemma less_than_singleton:
-  (X:(Ensemble U)) (x:U) (Strict_Included U X (Singleton U x)) ->
-  X ==(Empty_set U).
-Intros X x H'; Try Assumption.
-Red in H'.
-LApply (Singleton_atomic x (Full_set U));
- [Intro H'2; Try Exact H'2 | Apply Full_intro].
-Elim H'; Intros H'0 H'1; Try Exact H'1; Clear H'.
-Elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
- [Intros H'6 H'7; Try Exact H'7 | Idtac]; Auto with sets.
-Elim (H'7 X); [Intro H'5; Try Exact H'5 | Intro H'5 | Idtac | Idtac]; Auto with sets.
-Elim H'1; Auto with sets.
+Lemma less_than_singleton :
+ forall (X:Ensemble U) (x:U),
+   Strict_Included U X (Singleton U x) -> X = Empty_set U.
+intros X x H'; try assumption.
+red in H'.
+lapply (Singleton_atomic x (Full_set U));
+ [ intro H'2; try exact H'2 | apply Full_intro ].
+elim H'; intros H'0 H'1; try exact H'1; clear H'.
+elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
+ [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets.
+elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ];
+ auto with sets.
+elim H'1; auto with sets.
 Qed.
 
 End Sets_as_an_algebra.
 
-Hints Resolve incl_soustr_in : sets v62.
-Hints Resolve incl_soustr : sets v62.
-Hints Resolve incl_soustr_add_l : sets v62.
-Hints Resolve incl_soustr_add_r : sets v62.
-Hints Resolve add_soustr_1 add_soustr_2 : sets v62.
-Hints Resolve add_soustr_xy : sets v62.
+Hint Resolve incl_soustr_in: sets v62.
+Hint Resolve incl_soustr: sets v62.
+Hint Resolve incl_soustr_add_l: sets v62.
+Hint Resolve incl_soustr_add_r: sets v62.
+Hint Resolve add_soustr_1 add_soustr_2: sets v62.
+Hint Resolve add_soustr_xy: sets v62.
\ No newline at end of file
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 3e1837078..c587744a3 100755
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -35,242 +35,234 @@ Require Export Cpo.
 Require Export Powerset.
 
 Section Sets_as_an_algebra.
-Variable U: Type.
-Hints Unfold not.
+Variable U : Type.
+Hint Unfold not.
 
-Theorem Empty_set_zero :
-  (X: (Ensemble U)) (Union U (Empty_set U) X) == X.
+Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X.
 Proof.
-Auto 6 with sets.
+auto 6 with sets.
 Qed.
-Hints Resolve Empty_set_zero.
+Hint Resolve Empty_set_zero.
 
-Theorem Empty_set_zero' :
-  (x: U) (Add U (Empty_set U) x) == (Singleton U x).
+Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
 Proof.
-Unfold 1 Add; Auto with sets.
+unfold Add at 1 in |- *; auto with sets.
 Qed.
-Hints Resolve Empty_set_zero'.
+Hint Resolve Empty_set_zero'.
 
 Lemma less_than_empty :
-  (X: (Ensemble U)) (Included U X (Empty_set U)) -> X == (Empty_set U).
+ forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
-Hints Resolve less_than_empty.
+Hint Resolve less_than_empty.
 
-Theorem Union_commutative :
-  (A,B: (Ensemble U)) (Union U A B) == (Union U B A).
+Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
 
 Theorem Union_associative :
-  (A, B, C: (Ensemble U))
-  (Union U (Union U A B) C) == (Union U A (Union U B C)).
+ forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
 Proof.
-Auto 9 with sets.
+auto 9 with sets.
 Qed.
-Hints Resolve Union_associative.
+Hint Resolve Union_associative.
 
-Theorem Union_idempotent : (A: (Ensemble U)) (Union U A A) == A.
+Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.
 Proof.
-Auto 7 with sets.
+auto 7 with sets.
 Qed.
 
 Lemma Union_absorbs :
-  (A, B: (Ensemble U)) (Included U B A) -> (Union U A B) == A.
+ forall A B:Ensemble U, Included U B A -> Union U A B = A.
 Proof.
-Auto 7 with sets.
+auto 7 with sets.
 Qed.
 
-Theorem Couple_as_union:
-  (x, y: U) (Union U (Singleton U x) (Singleton U y)) == (Couple U x y).
+Theorem Couple_as_union :
+ forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
 Proof.
-Intros x y; Apply Extensionality_Ensembles; Split; Red.
-Intros x0 H'; Elim H'; (Intros x1 H'0; Elim H'0; Auto with sets).
-Intros x0 H'; Elim H'; Auto with sets.
+intros x y; apply Extensionality_Ensembles; split; red in |- *.
+intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
+intros x0 H'; elim H'; auto with sets.
 Qed.
 
 Theorem Triple_as_union :
-  (x, y, z: U)
-  (Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z)) ==
-  (Triple U x y z).
+ forall x y z:U,
+   Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
+   Triple U x y z.
 Proof.
-Intros x y z; Apply Extensionality_Ensembles; Split; Red.
-Intros x0 H'; Elim H'.
-Intros x1 H'0; Elim H'0; (Intros x2 H'1; Elim H'1; Auto with sets).
-Intros x1 H'0; Elim H'0; Auto with sets.
-Intros x0 H'; Elim H'; Auto with sets.
+intros x y z; apply Extensionality_Ensembles; split; red in |- *.
+intros x0 H'; elim H'.
+intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
+intros x1 H'0; elim H'0; auto with sets.
+intros x0 H'; elim H'; auto with sets.
 Qed.
 
-Theorem Triple_as_Couple : (x, y: U) (Couple U x y) == (Triple U x x y).
+Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
 Proof.
-Intros x y.
-Rewrite <- (Couple_as_union x y).
-Rewrite <- (Union_idempotent (Singleton U x)).
-Apply Triple_as_union.
+intros x y.
+rewrite <- (Couple_as_union x y).
+rewrite <- (Union_idempotent (Singleton U x)).
+apply Triple_as_union.
 Qed.
 
 Theorem Triple_as_Couple_Singleton :
-  (x, y, z: U) (Triple U x y z) == (Union U (Couple U x y) (Singleton U z)).
+ forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
 Proof.
-Intros x y z.
-Rewrite <- (Triple_as_union x y z).
-Rewrite <- (Couple_as_union x y); Auto with sets.
+intros x y z.
+rewrite <- (Triple_as_union x y z).
+rewrite <- (Couple_as_union x y); auto with sets.
 Qed.
 
 Theorem Intersection_commutative :
-  (A,B: (Ensemble U)) (Intersection U A B) == (Intersection U B A).
+ forall A B:Ensemble U, Intersection U A B = Intersection U B A.
 Proof.
-Intros A B.
-Apply Extensionality_Ensembles.
-Split; Red; Intros x H'; Elim H'; Auto with sets.
+intros A B.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x H'; elim H'; auto with sets.
 Qed.
 
 Theorem Distributivity :
-  (A, B, C: (Ensemble U))
-     (Intersection U A (Union U B C)) ==
-     (Union U (Intersection U A B) (Intersection U A C)).
+ forall A B C:Ensemble U,
+   Intersection U A (Union U B C) =
+   Union U (Intersection U A B) (Intersection U A C).
 Proof.
-Intros A B C.
-Apply Extensionality_Ensembles.
-Split; Red; Intros x H'.
-Elim H'.
-Intros x0 H'0 H'1; Generalize H'0.
-Elim H'1; Auto with sets.
-Elim H'; Intros x0 H'0; Elim H'0; Auto with sets.
+intros A B C.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x H'.
+elim H'.
+intros x0 H'0 H'1; generalize H'0.
+elim H'1; auto with sets.
+elim H'; intros x0 H'0; elim H'0; auto with sets.
 Qed.
 
 Theorem Distributivity' :
-  (A, B, C: (Ensemble U))
-     (Union U A (Intersection U B C)) ==
-     (Intersection U (Union U A B) (Union U A C)).
+ forall A B C:Ensemble U,
+   Union U A (Intersection U B C) =
+   Intersection U (Union U A B) (Union U A C).
 Proof.
-Intros A B C.
-Apply Extensionality_Ensembles.
-Split; Red; Intros x H'.
-Elim H'; Auto with sets.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Elim H'.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intros x1 H'1 H'2; Try Exact H'2.
-Generalize H'1.
-Elim H'2; Auto with sets.
+intros A B C.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x H'.
+elim H'; auto with sets.
+intros x0 H'0; elim H'0; auto with sets.
+elim H'.
+intros x0 H'0; elim H'0; auto with sets.
+intros x1 H'1 H'2; try exact H'2.
+generalize H'1.
+elim H'2; auto with sets.
 Qed.
 
 Theorem Union_add :
-  (A, B: (Ensemble U)) (x: U)
-    (Add U (Union U A B) x) == (Union U A (Add U B x)).
+ forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
 Proof.
-Unfold Add; Auto with sets.
+unfold Add in |- *; auto with sets.
 Qed.
-Hints Resolve Union_add.
+Hint Resolve Union_add.
 
 Theorem Non_disjoint_union :
-  (X: (Ensemble U)) (x: U) (In U X x) -> (Add U X x) == X.
-Intros X x H'; Unfold Add.
-Apply Extensionality_Ensembles; Red.
-Split; Red; Auto with sets.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intros t H'1; Elim H'1; Auto with sets.
+ forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
+intros X x H'; unfold Add in |- *.
+apply Extensionality_Ensembles; red in |- *.
+split; red in |- *; auto with sets.
+intros x0 H'0; elim H'0; auto with sets.
+intros t H'1; elim H'1; auto with sets.
 Qed.
 
 Theorem Non_disjoint_union' :
-  (X: (Ensemble U)) (x: U) ~ (In U X x) -> (Subtract U X x) == X.
+ forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
 Proof.
-Intros X x H'; Unfold Subtract.
-Apply Extensionality_Ensembles.
-Split; Red; Auto with sets.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intros x0 H'0; Apply Setminus_intro; Auto with sets.
-Red; Intro H'1; Elim H'1.
-LApply (Singleton_inv U x x0); Auto with sets.
-Intro H'4; Apply H'; Rewrite H'4; Auto with sets.
+intros X x H'; unfold Subtract in |- *.
+apply Extensionality_Ensembles.
+split; red in |- *; auto with sets.
+intros x0 H'0; elim H'0; auto with sets.
+intros x0 H'0; apply Setminus_intro; auto with sets.
+red in |- *; intro H'1; elim H'1.
+lapply (Singleton_inv U x x0); auto with sets.
+intro H'4; apply H'; rewrite H'4; auto with sets.
 Qed.
 
-Lemma singlx : (x, y: U) (In U (Add U (Empty_set U) x) y) -> x == y.
+Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
 Proof.
-Intro x; Rewrite (Empty_set_zero' x); Auto with sets.
+intro x; rewrite (Empty_set_zero' x); auto with sets.
 Qed.
-Hints Resolve singlx.
+Hint Resolve singlx.
 
 Lemma incl_add :
-  (A, B: (Ensemble U)) (x: U) (Included U A B) ->
-   (Included U (Add U A x) (Add U B x)).
+ forall (A B:Ensemble U) (x:U),
+   Included U A B -> Included U (Add U A x) (Add U B x).
 Proof.
-Intros A B x H'; Red; Auto with sets.
-Intros x0 H'0.
-LApply (Add_inv U A x x0); Auto with sets.
-Intro H'1; Elim H'1;
- [Intro H'2; Clear H'1 | Intro H'2; Rewrite <- H'2; Clear H'1]; Auto with sets.
+intros A B x H'; red in |- *; auto with sets.
+intros x0 H'0.
+lapply (Add_inv U A x x0); auto with sets.
+intro H'1; elim H'1;
+ [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ];
+ auto with sets.
 Qed.
-Hints Resolve incl_add.
+Hint Resolve incl_add.
 
 Lemma incl_add_x :
-  (A, B: (Ensemble U))
-  (x: U) ~ (In U A x) -> (Included U (Add U A x) (Add U B x)) ->
-   (Included U A B).
+ forall (A B:Ensemble U) (x:U),
+   ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
 Proof.
-Unfold Included.
-Intros A B x H' H'0 x0 H'1.
-LApply (H'0 x0); Auto with sets.
-Intro H'2; LApply (Add_inv U B x x0); Auto with sets.
-Intro H'3; Elim H'3;
- [Intro H'4; Try Exact H'4; Clear H'3 | Intro H'4; Clear H'3].
-Absurd (In U A x0); Auto with sets.
-Rewrite <- H'4; Auto with sets.
+unfold Included in |- *.
+intros A B x H' H'0 x0 H'1.
+lapply (H'0 x0); auto with sets.
+intro H'2; lapply (Add_inv U B x x0); auto with sets.
+intro H'3; elim H'3;
+ [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ].
+absurd (In U A x0); auto with sets.
+rewrite <- H'4; auto with sets.
 Qed.
 
 Lemma Add_commutative :
-  (A: (Ensemble U)) (x, y: U) (Add U (Add U A x) y) == (Add U (Add U A y) x).
+ forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
 Proof.
-Intros A x y.
-Unfold Add.
-Rewrite (Union_associative A (Singleton U x) (Singleton U y)).
-Rewrite (Union_commutative (Singleton U x) (Singleton U y)).
-Rewrite <- (Union_associative A (Singleton U y) (Singleton U x)); Auto with sets.
+intros A x y.
+unfold Add in |- *.
+rewrite (Union_associative A (Singleton U x) (Singleton U y)).
+rewrite (Union_commutative (Singleton U x) (Singleton U y)).
+rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
+ auto with sets.
 Qed.
 
 Lemma Add_commutative' :
-  (A: (Ensemble U)) (x, y, z: U)
-    (Add U (Add U (Add U A x) y) z) == (Add U (Add U (Add U A z) x) y).
+ forall (A:Ensemble U) (x y z:U),
+   Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.
 Proof.
-Intros A x y z.
-Rewrite (Add_commutative (Add U A x) y z).
-Rewrite (Add_commutative A x z); Auto with sets.
+intros A x y z.
+rewrite (Add_commutative (Add U A x) y z).
+rewrite (Add_commutative A x z); auto with sets.
 Qed.
 
 Lemma Add_distributes :
-  (A, B: (Ensemble U)) (x, y: U) (Included U B A) ->
-  (Add U (Add U A x) y) == (Union U (Add U A x) (Add U B y)).
+ forall (A B:Ensemble U) (x y:U),
+   Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
 Proof.
-Intros A B x y H'; Try Assumption.
-Rewrite <- (Union_add (Add U A x) B y).
-Unfold 4 Add.
-Rewrite (Union_commutative A (Singleton U x)).
-Rewrite Union_associative.
-Rewrite (Union_absorbs A B H').
-Rewrite (Union_commutative (Singleton U x) A).
-Auto with sets.
+intros A B x y H'; try assumption.
+rewrite <- (Union_add (Add U A x) B y).
+unfold Add at 4 in |- *.
+rewrite (Union_commutative A (Singleton U x)).
+rewrite Union_associative.
+rewrite (Union_absorbs A B H').
+rewrite (Union_commutative (Singleton U x) A).
+auto with sets.
 Qed.
 
 Lemma setcover_intro :
-  (U: Type)
-  (A: (Ensemble U))
-  (x, y: (Ensemble U))
-  (Strict_Included U x y) ->
-  ~ (EXT z | (Strict_Included U x z) 
-              /\ (Strict_Included U z y)) ->
-   (covers (Ensemble U) (Power_set_PO U A) y x).
+ forall (U:Type) (A x y:Ensemble U),
+   Strict_Included U x y ->
+   ~ ( exists z : _ | Strict_Included U x z /\ Strict_Included U z y) ->
+   covers (Ensemble U) (Power_set_PO U A) y x.
 Proof.
-Intros; Apply Definition_of_covers; Auto with sets.
+intros; apply Definition_of_covers; auto with sets.
 Qed.
-Hints Resolve setcover_intro.
+Hint Resolve setcover_intro.
 
 End Sets_as_an_algebra.
 
-Hints Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
-	singlx incl_add : sets v62.
-
+Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
+  singlx incl_add: sets v62.
 
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 74c031726..16a00740d 100755
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -27,41 +27,41 @@
 (*i $Id$ i*)
 
 Section Relations_1.
-   Variable U: Type.
+   Variable U : Type.
    
-   Definition Relation :=  U -> U -> Prop.
-   Variable R: Relation.
+   Definition Relation := U -> U -> Prop.
+   Variable R : Relation.
    
-   Definition Reflexive : Prop :=  (x: U) (R x x).
+   Definition Reflexive : Prop := forall x:U, R x x.
    
-   Definition Transitive : Prop :=  (x,y,z: U) (R x y) -> (R y z) -> (R x z).
+   Definition Transitive : Prop := forall x y z:U, R x y -> R y z -> R x z.
    
-   Definition Symmetric : Prop :=  (x,y: U) (R x y) -> (R y x).
+   Definition Symmetric : Prop := forall x y:U, R x y -> R y x.
    
-   Definition Antisymmetric : Prop :=
-      (x: U) (y: U) (R x y) -> (R y x) -> x == y.
+   Definition Antisymmetric : Prop := forall x y:U, R x y -> R y x -> x = y.
    
-   Definition contains : Relation -> Relation -> Prop :=
-      [R,R': Relation] (x: U) (y: U) (R' x y) -> (R x y).
+   Definition contains (R R':Relation) : Prop :=
+     forall x y:U, R' x y -> R x y.
    
-   Definition same_relation : Relation -> Relation -> Prop :=
-      [R,R': Relation] (contains R R') /\ (contains R' R).
+   Definition same_relation (R R':Relation) : Prop :=
+     contains R R' /\ contains R' R.
    
    Inductive Preorder : Prop :=
-         Definition_of_preorder: Reflexive -> Transitive -> Preorder.
+       Definition_of_preorder : Reflexive -> Transitive -> Preorder.
    
    Inductive Order : Prop :=
-         Definition_of_order: Reflexive -> Transitive -> Antisymmetric -> Order.
+       Definition_of_order :
+         Reflexive -> Transitive -> Antisymmetric -> Order.
    
    Inductive Equivalence : Prop :=
-         Definition_of_equivalence:
-           Reflexive -> Transitive -> Symmetric -> Equivalence.
+       Definition_of_equivalence :
+         Reflexive -> Transitive -> Symmetric -> Equivalence.
    
    Inductive PER : Prop :=
-         Definition_of_PER: Symmetric -> Transitive -> PER.
+       Definition_of_PER : Symmetric -> Transitive -> PER.
    
 End Relations_1.
-Hints Unfold Reflexive Transitive Antisymmetric Symmetric contains 
-	same_relation : sets v62.
-Hints Resolve Definition_of_preorder Definition_of_order 
-	Definition_of_equivalence Definition_of_PER : sets v62.
+Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
+  same_relation: sets v62.
+Hint Resolve Definition_of_preorder Definition_of_order
+  Definition_of_equivalence Definition_of_PER: sets v62.
\ No newline at end of file
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index b490fa7a0..61557aff7 100755
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -28,82 +28,85 @@
 
 Require Export Relations_1.
 
-Definition Complement : (U: Type) (Relation U) -> (Relation U) :=
-   [U: Type] [R: (Relation U)] [x,y: U] ~ (R x y).
+Definition Complement (U:Type) (R:Relation U) : Relation U :=
+  fun x y:U => ~ R x y.
 
-Theorem Rsym_imp_notRsym: (U: Type) (R: (Relation U)) (Symmetric U R) ->
-            (Symmetric U (Complement U R)).
+Theorem Rsym_imp_notRsym :
+ forall (U:Type) (R:Relation U),
+   Symmetric U R -> Symmetric U (Complement U R).
 Proof.
-Unfold Symmetric Complement.
-Intros U R H' x y H'0; Red; Intro H'1; Apply H'0; Auto with sets.
+unfold Symmetric, Complement in |- *.
+intros U R H' x y H'0; red in |- *; intro H'1; apply H'0; auto with sets.
 Qed.
 
 Theorem Equiv_from_preorder :
-  (U: Type) (R: (Relation U)) (Preorder U R) ->
-            (Equivalence U [x,y: U] (R x y) /\ (R y x)).
+ forall (U:Type) (R:Relation U),
+   Preorder U R -> Equivalence U (fun x y:U => R x y /\ R y x).
 Proof.
-Intros U R H'; Elim H'; Intros H'0 H'1.
-Apply Definition_of_equivalence.
-Red in H'0; Auto 10 with sets.
-2:Red; Intros x y h; Elim h; Intros H'3 H'4; Auto 10 with sets.
-Red in H'1; Red; Auto 10 with sets.
-Intros x y z h; Elim h; Intros H'3 H'4; Clear h.
-Intro h; Elim h; Intros H'5 H'6; Clear h.
-Split; Apply H'1 with y; Auto 10 with sets.
+intros U R H'; elim H'; intros H'0 H'1.
+apply Definition_of_equivalence.
+red in H'0; auto 10 with sets.
+2: red in |- *; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
+red in H'1; red in |- *; auto 10 with sets.
+intros x y z h; elim h; intros H'3 H'4; clear h.
+intro h; elim h; intros H'5 H'6; clear h.
+split; apply H'1 with y; auto 10 with sets.
 Qed.
-Hints Resolve Equiv_from_preorder.
+Hint Resolve Equiv_from_preorder.
 
 Theorem Equiv_from_order :
-  (U: Type) (R: (Relation U)) (Order U R) ->
-            (Equivalence U [x,y: U] (R x y) /\ (R y x)).
+ forall (U:Type) (R:Relation U),
+   Order U R -> Equivalence U (fun x y:U => R x y /\ R y x).
 Proof.
-Intros U R H'; Elim H'; Auto 10 with sets.
+intros U R H'; elim H'; auto 10 with sets.
 Qed.
-Hints Resolve Equiv_from_order.
+Hint Resolve Equiv_from_order.
 
 Theorem contains_is_preorder :
-  (U: Type) (Preorder (Relation U) (contains U)).
+ forall U:Type, Preorder (Relation U) (contains U).
 Proof.
-Auto 10 with sets.
+auto 10 with sets.
 Qed.
-Hints Resolve contains_is_preorder.
+Hint Resolve contains_is_preorder.
 
 Theorem same_relation_is_equivalence :
-  (U: Type) (Equivalence (Relation U) (same_relation U)).
+ forall U:Type, Equivalence (Relation U) (same_relation U).
 Proof.
-Unfold 1 same_relation; Auto 10 with sets.
+unfold same_relation at 1 in |- *; auto 10 with sets.
 Qed.
-Hints Resolve same_relation_is_equivalence.
+Hint Resolve same_relation_is_equivalence.
 
-Theorem cong_reflexive_same_relation:
-  (U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Reflexive U R) ->
-  (Reflexive U R').
+Theorem cong_reflexive_same_relation :
+ forall (U:Type) (R R':Relation U),
+   same_relation U R R' -> Reflexive U R -> Reflexive U R'.
 Proof.
-Unfold same_relation; Intuition.
+unfold same_relation in |- *; intuition.
 Qed.
 
-Theorem cong_symmetric_same_relation:
-  (U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Symmetric U R) ->
-  (Symmetric U R').
+Theorem cong_symmetric_same_relation :
+ forall (U:Type) (R R':Relation U),
+   same_relation U R R' -> Symmetric U R -> Symmetric U R'.
 Proof.
-  Compute;Intros;Elim H;Intros;Clear H;Apply (H3 y x (H0 x y (H2 x y H1))).
+  compute in |- *; intros; elim H; intros; clear H;
+   apply (H3 y x (H0 x y (H2 x y H1))).
 (*Intuition.*)
 Qed.
 
-Theorem cong_antisymmetric_same_relation:
-  (U:Type) (R, R':(Relation U)) (same_relation U R R') ->
-           (Antisymmetric U R) -> (Antisymmetric U R').
+Theorem cong_antisymmetric_same_relation :
+ forall (U:Type) (R R':Relation U),
+   same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'.
 Proof.
-  Compute;Intros;Elim H;Intros;Clear H;Apply (H0 x y (H3 x y H1) (H3 y x H2)).
+  compute in |- *; intros; elim H; intros; clear H;
+   apply (H0 x y (H3 x y H1) (H3 y x H2)).
 (*Intuition.*)
 Qed.
 
-Theorem cong_transitive_same_relation:
-  (U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Transitive U R) ->
-  (Transitive U R').
+Theorem cong_transitive_same_relation :
+ forall (U:Type) (R R':Relation U),
+   same_relation U R R' -> Transitive U R -> Transitive U R'.
 Proof.
-Intros U R R' H' H'0; Red.
-Elim H'.
-Intros H'1 H'2 x y z H'3 H'4; Apply H'2.
-Apply H'0 with y; Auto with sets.
-Qed.
+intros U R R' H' H'0; red in |- *.
+elim H'.
+intros H'1 H'2 x y z H'3 H'4; apply H'2.
+apply H'0 with y; auto with sets.
+Qed.
\ No newline at end of file
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 65363d816..d7ee68b66 100755
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -29,28 +29,28 @@
 Require Export Relations_1.
 
 Section Relations_2.
-Variable U: Type.
-Variable R: (Relation U).
+Variable U : Type.
+Variable R : Relation U.
 
-Inductive Rstar : (Relation U) :=
-     Rstar_0: (x: U) (Rstar x x)
-   | Rstar_n: (x, y, z: U) (R x y) -> (Rstar y z) -> (Rstar x z).
+Inductive Rstar : Relation U :=
+  | Rstar_0 : forall x:U, Rstar x x
+  | Rstar_n : forall x y z:U, R x y -> Rstar y z -> Rstar x z.
 
-Inductive Rstar1 : (Relation U) :=
-     Rstar1_0: (x: U) (Rstar1 x x)
-   | Rstar1_1: (x: U) (y: U) (R x y) -> (Rstar1 x y)
-   | Rstar1_n: (x, y, z: U) (Rstar1 x y) -> (Rstar1 y z) -> (Rstar1 x z).
+Inductive Rstar1 : Relation U :=
+  | Rstar1_0 : forall x:U, Rstar1 x x
+  | Rstar1_1 : forall x y:U, R x y -> Rstar1 x y
+  | Rstar1_n : forall x y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z.
 
-Inductive Rplus : (Relation U) :=
-     Rplus_0: (x, y: U) (R x y) -> (Rplus x y)
-   | Rplus_n: (x, y, z: U) (R x y) -> (Rplus y z) -> (Rplus x z).
+Inductive Rplus : Relation U :=
+  | Rplus_0 : forall x y:U, R x y -> Rplus x y
+  | Rplus_n : forall x y z:U, R x y -> Rplus y z -> Rplus x z.
 
 Definition Strongly_confluent : Prop :=
-   (x, a, b: U) (R x a) -> (R x b) -> (exT U [z: U] (R a z) /\ (R b z)).
+  forall x a b:U, R x a -> R x b -> ex (fun z:U => R a z /\ R b z).
 
 End Relations_2.
 
-Hints Resolve Rstar_0 : sets v62.
-Hints Resolve Rstar1_0 : sets v62.
-Hints Resolve Rstar1_1 : sets v62.
-Hints Resolve Rplus_0 : sets v62.
+Hint Resolve Rstar_0: sets v62.
+Hint Resolve Rstar1_0: sets v62.
+Hint Resolve Rstar1_1: sets v62.
+Hint Resolve Rplus_0: sets v62.
\ No newline at end of file
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 588b7f431..4fda8d8e9 100755
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -30,122 +30,124 @@ Require Export Relations_1.
 Require Export Relations_1_facts.
 Require Export Relations_2.
 
-Theorem Rstar_reflexive : 
-  (U: Type) (R: (Relation U)) (Reflexive U (Rstar U R)).
+Theorem Rstar_reflexive :
+ forall (U:Type) (R:Relation U), Reflexive U (Rstar U R).
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
 
 Theorem Rplus_contains_R :
-  (U: Type) (R: (Relation U)) (contains U (Rplus U R) R).
+ forall (U:Type) (R:Relation U), contains U (Rplus U R) R.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
 
 Theorem Rstar_contains_R :
-  (U: Type) (R: (Relation U)) (contains U (Rstar U R) R).
+ forall (U:Type) (R:Relation U), contains U (Rstar U R) R.
 Proof.
-Intros U R; Red; Intros x y H'; Apply Rstar_n with y; Auto with sets.
+intros U R; red in |- *; intros x y H'; apply Rstar_n with y; auto with sets.
 Qed.
 
 Theorem Rstar_contains_Rplus :
-  (U: Type) (R: (Relation U)) (contains U (Rstar U R) (Rplus U R)).
+ forall (U:Type) (R:Relation U), contains U (Rstar U R) (Rplus U R).
 Proof.
-Intros U R; Red.
-Intros x y H'; Elim H'.
-Generalize Rstar_contains_R; Intro T; Red in T; Auto with sets.
-Intros x0 y0 z H'0 H'1 H'2; Apply Rstar_n with y0; Auto with sets.
+intros U R; red in |- *.
+intros x y H'; elim H'.
+generalize Rstar_contains_R; intro T; red in T; auto with sets.
+intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets.
 Qed.
 
 Theorem Rstar_transitive :
-  (U: Type) (R: (Relation U)) (Transitive U (Rstar U R)).
+ forall (U:Type) (R:Relation U), Transitive U (Rstar U R).
 Proof.
-Intros U R; Red.
-Intros x y z H'; Elim H'; Auto with sets.
-Intros x0 y0 z0 H'0 H'1 H'2 H'3; Apply Rstar_n with y0; Auto with sets.
+intros U R; red in |- *.
+intros x y z H'; elim H'; auto with sets.
+intros x0 y0 z0 H'0 H'1 H'2 H'3; apply Rstar_n with y0; auto with sets.
 Qed.
 
 Theorem Rstar_cases :
-  (U: Type) (R: (Relation U)) (x, y: U) (Rstar U R x y) ->
-    x == y \/ (EXT u | (R x u) /\ (Rstar U R u y)).
+ forall (U:Type) (R:Relation U) (x y:U),
+   Rstar U R x y -> x = y \/ ( exists u : _ | R x u /\ Rstar U R u y).
 Proof.
-Intros U R x y H'; Elim H'; Auto with sets.
-Intros x0 y0 z H'0 H'1 H'2; Right; Exists y0; Auto with sets.
+intros U R x y H'; elim H'; auto with sets.
+intros x0 y0 z H'0 H'1 H'2; right; exists y0; auto with sets.
 Qed.
 
 Theorem Rstar_equiv_Rstar1 :
-  (U: Type) (R: (Relation U)) (same_relation U (Rstar U R) (Rstar1 U R)).
+ forall (U:Type) (R:Relation U), same_relation U (Rstar U R) (Rstar1 U R).
 Proof.
-Generalize Rstar_contains_R; Intro T; Red in T.
-Intros U R; Unfold same_relation contains.
-Split; Intros x y H'; Elim H'; Auto with sets.
-Generalize Rstar_transitive; Intro T1; Red in T1.
-Intros x0 y0 z H'0 H'1 H'2 H'3; Apply T1 with y0; Auto with sets.
-Intros x0 y0 z H'0 H'1 H'2; Apply Rstar1_n with y0; Auto with sets.
+generalize Rstar_contains_R; intro T; red in T.
+intros U R; unfold same_relation, contains in |- *.
+split; intros x y H'; elim H'; auto with sets.
+generalize Rstar_transitive; intro T1; red in T1.
+intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets.
+intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets.
 Qed.
 
 Theorem Rsym_imp_Rstarsym :
-  (U: Type) (R: (Relation U)) (Symmetric U R) -> (Symmetric U (Rstar U R)).
+ forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Rstar U R).
 Proof.
-Intros U R H'; Red.
-Intros x y H'0; Elim H'0; Auto with sets.
-Intros x0 y0 z H'1 H'2 H'3.
-Generalize Rstar_transitive; Intro T1; Red in T1.
-Apply T1 with y0; Auto with sets.
-Apply Rstar_n with x0; Auto with sets.
+intros U R H'; red in |- *.
+intros x y H'0; elim H'0; auto with sets.
+intros x0 y0 z H'1 H'2 H'3.
+generalize Rstar_transitive; intro T1; red in T1.
+apply T1 with y0; auto with sets.
+apply Rstar_n with x0; auto with sets.
 Qed.
 
 Theorem Sstar_contains_Rstar :
-  (U: Type) (R, S: (Relation U)) (contains U (Rstar U S) R) ->
-   (contains U (Rstar U S) (Rstar U R)).
+ forall (U:Type) (R S:Relation U),
+   contains U (Rstar U S) R -> contains U (Rstar U S) (Rstar U R).
 Proof.
-Unfold contains.
-Intros U R S H' x y H'0; Elim H'0; Auto with sets.
-Generalize Rstar_transitive; Intro T1; Red in T1.
-Intros x0 y0 z H'1 H'2 H'3; Apply T1 with y0; Auto with sets.
+unfold contains in |- *.
+intros U R S H' x y H'0; elim H'0; auto with sets.
+generalize Rstar_transitive; intro T1; red in T1.
+intros x0 y0 z H'1 H'2 H'3; apply T1 with y0; auto with sets.
 Qed.
 
 Theorem star_monotone :
-  (U: Type) (R, S: (Relation U)) (contains U S R) ->
-   (contains U (Rstar U S) (Rstar U R)).
+ forall (U:Type) (R S:Relation U),
+   contains U S R -> contains U (Rstar U S) (Rstar U R).
 Proof.
-Intros U R S H'.
-Apply Sstar_contains_Rstar; Auto with sets.
-Generalize (Rstar_contains_R U S); Auto with sets.
+intros U R S H'.
+apply Sstar_contains_Rstar; auto with sets.
+generalize (Rstar_contains_R U S); auto with sets.
 Qed.
 
 Theorem RstarRplus_RRstar :
-  (U: Type) (R: (Relation U)) (x, y, z: U) 
-    (Rstar U R x y) -> (Rplus U R y z) ->
-    (EXT u | (R x u) /\ (Rstar U R u z)).
+ forall (U:Type) (R:Relation U) (x y z:U),
+   Rstar U R x y -> Rplus U R y z ->  exists u : _ | R x u /\ Rstar U R u z.
 Proof.
-Generalize Rstar_contains_Rplus; Intro T; Red in T.
-Generalize Rstar_transitive; Intro T1; Red in T1.
-Intros U R x y z H'; Elim H'.
-Intros x0 H'0; Elim H'0.
-Intros x1 y0 H'1; Exists y0; Auto with sets.
-Intros x1 y0 z0 H'1 H'2 H'3; Exists y0; Auto with sets.
-Intros x0 y0 z0 H'0 H'1 H'2 H'3; Exists y0.
-Split; [Try Assumption | Idtac].
-Apply T1 with z0; Auto with sets.
+generalize Rstar_contains_Rplus; intro T; red in T.
+generalize Rstar_transitive; intro T1; red in T1.
+intros U R x y z H'; elim H'.
+intros x0 H'0; elim H'0.
+intros x1 y0 H'1; exists y0; auto with sets.
+intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets.
+intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0.
+split; [ try assumption | idtac ].
+apply T1 with z0; auto with sets.
 Qed.
 
-Theorem Lemma1 : 
-  (U: Type) (R: (Relation U)) (Strongly_confluent U R) ->
-   (x, b: U) (Rstar U R x b) ->
-    (a: U) (R x a) -> (EXT z | (Rstar U R a z) /\ (R b z)).
+Theorem Lemma1 :
+ forall (U:Type) (R:Relation U),
+   Strongly_confluent U R ->
+   forall x b:U,
+     Rstar U R x b ->
+     forall a:U, R x a ->  exists z : _ | Rstar U R a z /\ R b z.
 Proof.
-Intros U R H' x b H'0; Elim H'0.
-Intros x0 a H'1; Exists a; Auto with sets.
-Intros x0 y z H'1 H'2 H'3 a H'4.
-Red in H'.
-Specialize 3 H' with x := x0 a := a b := y; Intro H'7; LApply H'7;
- [Intro H'8; LApply H'8;
-   [Intro H'9; Try Exact H'9; Clear H'8 H'7 | Clear H'8 H'7] | Clear H'7]; Auto with sets.
-Elim H'9.
-Intros t H'5; Elim H'5; Intros H'6 H'7; Try Exact H'6; Clear H'5.
-Elim (H'3 t); Auto with sets.
-Intros z1 H'5; Elim H'5; Intros H'8 H'10; Try Exact H'8; Clear H'5.
-Exists z1; Split; [Idtac | Assumption].
-Apply Rstar_n with t; Auto with sets.
-Qed.
+intros U R H' x b H'0; elim H'0.
+intros x0 a H'1; exists a; auto with sets.
+intros x0 y z H'1 H'2 H'3 a H'4.
+red in H'.
+specialize  3H' with (x := x0) (a := a) (b := y); intro H'7; lapply H'7;
+ [ intro H'8; lapply H'8;
+    [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ]
+ | clear H'7 ]; auto with sets.
+elim H'9.
+intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
+elim (H'3 t); auto with sets.
+intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5.
+exists z1; split; [ idtac | assumption ].
+apply Rstar_n with t; auto with sets.
+Qed.
\ No newline at end of file
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 90c055775..1fe689002 100755
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -30,34 +30,33 @@ Require Export Relations_1.
 Require Export Relations_2.
 
 Section Relations_3.
-   Variable U: Type.
-   Variable R: (Relation U).
+   Variable U : Type.
+   Variable R : Relation U.
    
-   Definition coherent : U -> U -> Prop :=
-      [x,y: U]  (EXT z | (Rstar U R x z) /\ (Rstar U R y z)).
+   Definition coherent (x y:U) : Prop :=
+      exists z : _ | Rstar U R x z /\ Rstar U R y z.
    
-   Definition locally_confluent : U -> Prop :=
-      [x: U] (y,z: U) (R x y) -> (R x z) -> (coherent y z).
+   Definition locally_confluent (x:U) : Prop :=
+     forall y z:U, R x y -> R x z -> coherent y z.
    
-   Definition Locally_confluent : Prop :=  (x: U) (locally_confluent x).
+   Definition Locally_confluent : Prop := forall x:U, locally_confluent x.
    
-   Definition confluent : U -> Prop :=
-      [x: U] (y,z: U) (Rstar U R x y) -> (Rstar U R x z) -> (coherent y z).
+   Definition confluent (x:U) : Prop :=
+     forall y z:U, Rstar U R x y -> Rstar U R x z -> coherent y z.
    
-   Definition Confluent : Prop :=  (x: U) (confluent x).
+   Definition Confluent : Prop := forall x:U, confluent x.
    
-   Inductive  noetherian : U -> Prop :=
-         definition_of_noetherian:
-           (x: U) ((y: U) (R x y) -> (noetherian y)) -> (noetherian x).
+   Inductive noetherian : U -> Prop :=
+       definition_of_noetherian :
+         forall x:U, (forall y:U, R x y -> noetherian y) -> noetherian x.
    
-   Definition Noetherian : Prop :=  (x: U) (noetherian x).
+   Definition Noetherian : Prop := forall x:U, noetherian x.
    
 End Relations_3.
-Hints Unfold  coherent : sets v62.
-Hints Unfold  locally_confluent : sets v62.
-Hints Unfold  confluent : sets v62.
-Hints Unfold  Confluent : sets v62.
-Hints Resolve definition_of_noetherian : sets v62.
-Hints Unfold  Noetherian : sets v62.
-
+Hint Unfold coherent: sets v62.
+Hint Unfold locally_confluent: sets v62.
+Hint Unfold confluent: sets v62.
+Hint Unfold Confluent: sets v62.
+Hint Resolve definition_of_noetherian: sets v62.
+Hint Unfold Noetherian: sets v62.
 
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index a57487d1e..5b1ce9e31 100755
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -33,125 +33,139 @@ Require Export Relations_2_facts.
 Require Export Relations_3.
 
 Theorem Rstar_imp_coherent :
-  (U: Type) (R: (Relation U)) (x: U) (y: U) (Rstar U R x y) ->
-   (coherent U R x y).
+ forall (U:Type) (R:Relation U) (x y:U), Rstar U R x y -> coherent U R x y.
 Proof.
-Intros U R x y H'; Red.
-Exists y; Auto with sets.
+intros U R x y H'; red in |- *.
+exists y; auto with sets.
 Qed.
-Hints Resolve Rstar_imp_coherent.
+Hint Resolve Rstar_imp_coherent.
 
 Theorem coherent_symmetric :
-  (U: Type) (R: (Relation U)) (Symmetric U (coherent U R)).
+ forall (U:Type) (R:Relation U), Symmetric U (coherent U R).
 Proof.
-Unfold 1 coherent.
-Intros U R; Red.
-Intros x y H'; Elim H'.
-Intros z H'0; Exists z; Tauto.
+unfold coherent at 1 in |- *.
+intros U R; red in |- *.
+intros x y H'; elim H'.
+intros z H'0; exists z; tauto.
 Qed.
 
 Theorem Strong_confluence :
-  (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R).
+ forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R.
 Proof.
-Intros U R H'; Red.
-Intro x; Red; Intros a b H'0.
-Unfold 1 coherent.
-Generalize b; Clear b.
-Elim H'0; Clear H'0.
-Intros x0 b H'1; Exists b; Auto with sets.
-Intros x0 y z H'1 H'2 H'3 b H'4.
-Generalize (Lemma1 U R); Intro h; LApply h;
-  [Intro H'0; Generalize (H'0 x0 b); Intro h0; LApply h0;
-    [Intro H'5; Generalize (H'5 y); Intro h1; LApply h1;
-      [Intro h2; Elim h2; Intros z0 h3; Elim h3; Intros H'6 H'7;
-        Clear h h0 h1 h2 h3 | Clear h h0 h1] | Clear h h0] | Clear h]; Auto with sets.
-Generalize (H'3 z0); Intro h; LApply h;
-  [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h h0 h1 |
-    Clear h]; Auto with sets.
-Exists z1; Split; Auto with sets.
-Apply Rstar_n with z0; Auto with sets.
+intros U R H'; red in |- *.
+intro x; red in |- *; intros a b H'0.
+unfold coherent at 1 in |- *.
+generalize b; clear b.
+elim H'0; clear H'0.
+intros x0 b H'1; exists b; auto with sets.
+intros x0 y z H'1 H'2 H'3 b H'4.
+generalize (Lemma1 U R); intro h; lapply h;
+ [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0;
+    [ intro H'5; generalize (H'5 y); intro h1; lapply h1;
+       [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7;
+          clear h h0 h1 h2 h3
+       | clear h h0 h1 ]
+    | clear h h0 ]
+ | clear h ]; auto with sets.
+generalize (H'3 z0); intro h; lapply h;
+ [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1
+ | clear h ]; auto with sets.
+exists z1; split; auto with sets.
+apply Rstar_n with z0; auto with sets.
 Qed.
 
 Theorem Strong_confluence_direct :
-  (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R).
+ forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R.
 Proof.
-Intros U R H'; Red.
-Intro x; Red; Intros a b H'0.
-Unfold 1 coherent.
-Generalize b; Clear b.
-Elim H'0; Clear H'0.
-Intros x0 b H'1; Exists b; Auto with sets.
-Intros x0 y z H'1 H'2 H'3 b H'4.
-Cut (exT U [t: U] (Rstar U R y t) /\ (R b t)).
-Intro h; Elim h; Intros t h0; Elim h0; Intros H'0 H'5; Clear h h0.
-Generalize (H'3 t); Intro h; LApply h;
-  [Intro h0; Elim h0; Intros z0 h1; Elim h1; Intros H'6 H'7; Clear h h0 h1 |
-    Clear h]; Auto with sets.
-Exists z0; Split; [Assumption | Idtac].
-Apply Rstar_n with t; Auto with sets.
-Generalize H'1; Generalize y; Clear H'1.
-Elim H'4.
-Intros x1 y0 H'0; Exists y0; Auto with sets.
-Intros x1 y0 z0 H'0 H'1 H'5 y1 H'6.
-Red in H'.
-Generalize (H' x1 y0 y1); Intro h; LApply h;
-  [Intro H'7; LApply H'7;
-    [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h H'7 h0 h1 |
-      Clear h] | Clear h]; Auto with sets.
-Generalize (H'5 z1); Intro h; LApply h;
-  [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'7 H'10; Clear h h0 h1 |
-    Clear h]; Auto with sets.
-Exists t; Split; Auto with sets.
-Apply Rstar_n with z1; Auto with sets.
+intros U R H'; red in |- *.
+intro x; red in |- *; intros a b H'0.
+unfold coherent at 1 in |- *.
+generalize b; clear b.
+elim H'0; clear H'0.
+intros x0 b H'1; exists b; auto with sets.
+intros x0 y z H'1 H'2 H'3 b H'4.
+cut (ex (fun t:U => Rstar U R y t /\ R b t)).
+intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0.
+generalize (H'3 t); intro h; lapply h;
+ [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1
+ | clear h ]; auto with sets.
+exists z0; split; [ assumption | idtac ].
+apply Rstar_n with t; auto with sets.
+generalize H'1; generalize y; clear H'1.
+elim H'4.
+intros x1 y0 H'0; exists y0; auto with sets.
+intros x1 y0 z0 H'0 H'1 H'5 y1 H'6.
+red in H'.
+generalize (H' x1 y0 y1); intro h; lapply h;
+ [ intro H'7; lapply H'7;
+    [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9;
+       clear h H'7 h0 h1
+    | clear h ]
+ | clear h ]; auto with sets.
+generalize (H'5 z1); intro h; lapply h;
+ [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1
+ | clear h ]; auto with sets.
+exists t; split; auto with sets.
+apply Rstar_n with z1; auto with sets.
 Qed.
 
 Theorem Noetherian_contains_Noetherian :
-  (U: Type) (R, R': (Relation U)) (Noetherian U R) -> (contains U R R') ->
-   (Noetherian U R').
+ forall (U:Type) (R R':Relation U),
+   Noetherian U R -> contains U R R' -> Noetherian U R'.
 Proof.
-Unfold 2 Noetherian.
-Intros U R R' H' H'0 x.
-Elim (H' x); Auto with sets.
+unfold Noetherian at 2 in |- *.
+intros U R R' H' H'0 x.
+elim (H' x); auto with sets.
 Qed.
 
 Theorem Newman :
-  (U: Type) (R: (Relation U)) (Noetherian U R) -> (Locally_confluent U R) ->
-   (Confluent U R).
+ forall (U:Type) (R:Relation U),
+   Noetherian U R -> Locally_confluent U R -> Confluent U R.
 Proof.
-Intros U R H' H'0; Red; Intro x.
-Elim (H' x); Unfold confluent.
-Intros x0 H'1 H'2 y z H'3 H'4.
-Generalize (Rstar_cases U R x0 y); Intro h; LApply h;
-  [Intro h0; Elim h0;
-    [Clear h h0; Intro h1 |
-      Intro h1; Elim h1; Intros u h2; Elim h2; Intros H'5 H'6; Clear h h0 h1 h2] |
-    Clear h]; Auto with sets.
-Elim h1; Auto with sets.
-Generalize (Rstar_cases U R x0 z); Intro h; LApply h;
-  [Intro h0; Elim h0;
-    [Clear h h0; Intro h1 |
-      Intro h1; Elim h1; Intros v h2; Elim h2; Intros H'7 H'8; Clear h h0 h1 h2] |
-    Clear h]; Auto with sets.
-Elim h1; Generalize coherent_symmetric; Intro t; Red in t; Auto with sets.
-Unfold Locally_confluent locally_confluent coherent in H'0.
-Generalize (H'0 x0 u v); Intro h; LApply h;
-  [Intro H'9; LApply H'9;
-    [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'10 H'11;
-      Clear h H'9 h0 h1 | Clear h] | Clear h]; Auto with sets.
-Clear H'0.
-Unfold 1 coherent in H'2.
-Generalize (H'2 u); Intro h; LApply h;
-  [Intro H'0; Generalize (H'0 y t); Intro h0; LApply h0;
-    [Intro H'9; LApply H'9;
-      [Intro h1; Elim h1; Intros y1 h2; Elim h2; Intros H'12 H'13;
-        Clear h h0 H'9 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets.
-Generalize Rstar_transitive; Intro T; Red in T.
-Generalize (H'2 v); Intro h; LApply h;
-  [Intro H'9; Generalize (H'9 y1 z); Intro h0; LApply h0;
-    [Intro H'14; LApply H'14;
-      [Intro h1; Elim h1; Intros z1 h2; Elim h2; Intros H'15 H'16;
-        Clear h h0 H'14 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets.
-Red; (Exists z1; Split); Auto with sets.
-Apply T with y1; Auto with sets.
-Apply T with t; Auto with sets.
-Qed.
+intros U R H' H'0; red in |- *; intro x.
+elim (H' x); unfold confluent in |- *.
+intros x0 H'1 H'2 y z H'3 H'4.
+generalize (Rstar_cases U R x0 y); intro h; lapply h;
+ [ intro h0; elim h0;
+    [ clear h h0; intro h1
+    | intro h1; elim h1; intros u h2; elim h2; intros H'5 H'6;
+       clear h h0 h1 h2 ]
+ | clear h ]; auto with sets.
+elim h1; auto with sets.
+generalize (Rstar_cases U R x0 z); intro h; lapply h;
+ [ intro h0; elim h0;
+    [ clear h h0; intro h1
+    | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8;
+       clear h h0 h1 h2 ]
+ | clear h ]; auto with sets.
+elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets.
+unfold Locally_confluent, locally_confluent, coherent in H'0.
+generalize (H'0 x0 u v); intro h; lapply h;
+ [ intro H'9; lapply H'9;
+    [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11;
+       clear h H'9 h0 h1
+    | clear h ]
+ | clear h ]; auto with sets.
+clear H'0.
+unfold coherent at 1 in H'2.
+generalize (H'2 u); intro h; lapply h;
+ [ intro H'0; generalize (H'0 y t); intro h0; lapply h0;
+    [ intro H'9; lapply H'9;
+       [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13;
+          clear h h0 H'9 h1 h2
+       | clear h h0 ]
+    | clear h h0 ]
+ | clear h ]; auto with sets.
+generalize Rstar_transitive; intro T; red in T.
+generalize (H'2 v); intro h; lapply h;
+ [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0;
+    [ intro H'14; lapply H'14;
+       [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16;
+          clear h h0 H'14 h1 h2
+       | clear h h0 ]
+    | clear h h0 ]
+ | clear h ]; auto with sets.
+red in |- *; (exists z1; split); auto with sets.
+apply T with y1; auto with sets.
+apply T with t; auto with sets.
+Qed.
\ No newline at end of file
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 5b28d6c2b..e1ba00209 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -13,7 +13,7 @@
 (* G. Huet 1-9-95 *)
 (* Updated Papageno 12/98 *)
 
-Require Bool.
+Require Import Bool.
 
 Set Implicit Arguments.
 
@@ -21,121 +21,118 @@ Section defs.
 
 Variable A : Set.
 Variable eqA : A -> A -> Prop.
-Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
-Inductive uniset : Set := 
-      Charac : (A->bool) -> uniset.
+Inductive uniset : Set :=
+    Charac : (A -> bool) -> uniset.
 
-Definition charac : uniset -> A -> bool :=
-  [s:uniset][a:A]Case s of [f:A->bool](f a) end.
+Definition charac (s:uniset) (a:A) : bool := let (f) := s in f a.
 
-Definition Emptyset := (Charac [a:A]false).
+Definition Emptyset := Charac (fun a:A => false).
 
-Definition Fullset  := (Charac [a:A]true).
+Definition Fullset := Charac (fun a:A => true).
 
-Definition Singleton := [a:A](Charac [a':A]
-              Case (eqA_dec a a') of 
-                   [h:(eqA a a')]  true
-                   [h: ~(eqA a a')] false end).
+Definition Singleton (a:A) :=
+  Charac
+    (fun a':A =>
+       match eqA_dec a a' with
+       | left h => true
+       | right h => false
+       end).
 
-Definition In : uniset -> A -> Prop :=
-     [s:uniset][a:A](charac s a)=true.
-Hints Unfold In.
+Definition In (s:uniset) (a:A) : Prop := charac s a = true.
+Hint Unfold In.
 
 (** uniset inclusion *)
-Definition incl := [s1,s2:uniset]
-    (a:A)(leb (charac s1 a) (charac s2 a)).
-Hints Unfold incl.
+Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a).
+Hint Unfold incl.
 
 (** uniset equality *)
-Definition seq := [s1,s2:uniset]
-    (a:A)(charac s1 a) = (charac s2 a).
-Hints Unfold seq.
+Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a.
+Hint Unfold seq.
 
-Lemma leb_refl : (b:bool)(leb b b).
+Lemma leb_refl : forall b:bool, leb b b.
 Proof.
-NewDestruct b; Simpl; Auto.
+destruct b; simpl in |- *; auto.
 Qed.
-Hints Resolve leb_refl.
+Hint Resolve leb_refl.
 
-Lemma incl_left : (s1,s2:uniset)(seq s1 s2)->(incl s1 s2).
+Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.
 Proof.
-Unfold incl; Intros s1 s2 E a; Elim (E a); Auto.
+unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
 Qed.
 
-Lemma incl_right : (s1,s2:uniset)(seq s1 s2)->(incl s2 s1).
+Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1.
 Proof.
-Unfold incl; Intros s1 s2 E a; Elim (E a); Auto.
+unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
 Qed.
 
-Lemma seq_refl : (x:uniset)(seq x x).
+Lemma seq_refl : forall x:uniset, seq x x.
 Proof.
-NewDestruct x; Unfold seq; Auto.
+destruct x; unfold seq in |- *; auto.
 Qed.
-Hints Resolve seq_refl.
+Hint Resolve seq_refl.
 
-Lemma seq_trans : (x,y,z:uniset)(seq x y)->(seq y z)->(seq x z).
+Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.
 Proof.
-Unfold seq.
-NewDestruct x; NewDestruct y; NewDestruct z; Simpl; Intros.
-Rewrite H; Auto.
+unfold seq in |- *.
+destruct x; destruct y; destruct z; simpl in |- *; intros.
+rewrite H; auto.
 Qed.
 
-Lemma seq_sym : (x,y:uniset)(seq x y)->(seq y x).
+Lemma seq_sym : forall x y:uniset, seq x y -> seq y x.
 Proof.
-Unfold seq.
-NewDestruct x; NewDestruct y; Simpl; Auto.
+unfold seq in |- *.
+destruct x; destruct y; simpl in |- *; auto.
 Qed.
 
 (** uniset union *)
-Definition union := [m1,m2:uniset]
-    (Charac [a:A](orb (charac m1 a)(charac m2 a))).
+Definition union (m1 m2:uniset) :=
+  Charac (fun a:A => orb (charac m1 a) (charac m2 a)).
 
-Lemma union_empty_left :
-     (x:uniset)(seq x (union Emptyset x)).  
+Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).  
 Proof.  
-Unfold seq; Unfold union; Simpl; Auto.  
+unfold seq in |- *; unfold union in |- *; simpl in |- *; auto.  
 Qed. 
-Hints Resolve union_empty_left.
+Hint Resolve union_empty_left.
 
-Lemma union_empty_right :
-     (x:uniset)(seq x (union x Emptyset)).
+Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
 Proof.
-Unfold seq; Unfold union; Simpl.
-Intros x a; Rewrite (orb_b_false (charac x a)); Auto.
+unfold seq in |- *; unfold union in |- *; simpl in |- *.
+intros x a; rewrite (orb_b_false (charac x a)); auto.
 Qed.
-Hints Resolve union_empty_right.
+Hint Resolve union_empty_right.
 
-Lemma union_comm : (x,y:uniset)(seq (union x y) (union y x)).
+Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).
 Proof.
-Unfold seq; Unfold charac; Unfold union.
-NewDestruct x; NewDestruct y; Auto with bool.
+unfold seq in |- *; unfold charac in |- *; unfold union in |- *.
+destruct x; destruct y; auto with bool.
 Qed.
-Hints Resolve union_comm.
+Hint Resolve union_comm.
 
-Lemma union_ass : 
-      (x,y,z:uniset)(seq (union (union x y) z) (union x (union y z))).
+Lemma union_ass :
+ forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).
 Proof.
-Unfold seq; Unfold union; Unfold charac.
-NewDestruct x; NewDestruct y; NewDestruct z; Auto with bool.
+unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+destruct x; destruct y; destruct z; auto with bool.
 Qed.
-Hints Resolve union_ass.
+Hint Resolve union_ass.
 
-Lemma seq_left :  (x,y,z:uniset)(seq x y)->(seq (union x z) (union y z)).
+Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).
 Proof.
-Unfold seq; Unfold union; Unfold charac.
-NewDestruct x; NewDestruct y; NewDestruct z.
-Intros; Elim H; Auto.
+unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+destruct x; destruct y; destruct z.
+intros; elim H; auto.
 Qed.
-Hints Resolve seq_left.
+Hint Resolve seq_left.
 
-Lemma seq_right : (x,y,z:uniset)(seq x y)->(seq (union z x) (union z y)).
+Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).
 Proof.
-Unfold seq; Unfold union; Unfold charac.
-NewDestruct x; NewDestruct y; NewDestruct z.
-Intros; Elim H; Auto.
+unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+destruct x; destruct y; destruct z.
+intros; elim H; auto.
 Qed.
-Hints Resolve seq_right.
+Hint Resolve seq_right.
 
 
 (** All the proofs that follow duplicate [Multiset_of_A] *)
@@ -143,60 +140,66 @@ Hints Resolve seq_right.
 (** Here we should make uniset an abstract datatype, by hiding [Charac],
     [union], [charac]; all further properties are proved abstractly *)
 
-Require Permut.
+Require Import Permut.
 
 Lemma union_rotate :
-   (x,y,z:uniset)(seq (union x (union y z)) (union z (union x y))).
+ forall x y z:uniset, seq (union x (union y z)) (union z (union x y)).
 Proof.
-Intros; Apply (op_rotate uniset union seq); Auto.
-Exact seq_trans.
+intros; apply (op_rotate uniset union seq); auto.
+exact seq_trans.
 Qed.
 
-Lemma seq_congr : (x,y,z,t:uniset)(seq x y)->(seq z t)->
-                  (seq (union x z) (union y t)).
+Lemma seq_congr :
+ forall x y z t:uniset, seq x y -> seq z t -> seq (union x z) (union y t).
 Proof.
-Intros; Apply (cong_congr uniset union seq); Auto.
-Exact seq_trans.
+intros; apply (cong_congr uniset union seq); auto.
+exact seq_trans.
 Qed.
 
 Lemma union_perm_left :
-   (x,y,z:uniset)(seq (union x (union y z)) (union y (union x z))).
+ forall x y z:uniset, seq (union x (union y z)) (union y (union x z)).
 Proof.
-Intros; Apply (perm_left uniset union seq); Auto.
-Exact seq_trans.
+intros; apply (perm_left uniset union seq); auto.
+exact seq_trans.
 Qed.
 
-Lemma uniset_twist1 : (x,y,z,t:uniset)
-   (seq (union x (union (union y z) t)) (union (union y (union x t)) z)).
+Lemma uniset_twist1 :
+ forall x y z t:uniset,
+   seq (union x (union (union y z) t)) (union (union y (union x t)) z).
 Proof.
-Intros; Apply (twist uniset union seq); Auto.
-Exact seq_trans.
+intros; apply (twist uniset union seq); auto.
+exact seq_trans.
 Qed.
 
-Lemma uniset_twist2 : (x,y,z,t:uniset)
-   (seq (union x (union (union y z) t)) (union (union y (union x z)) t)).
+Lemma uniset_twist2 :
+ forall x y z t:uniset,
+   seq (union x (union (union y z) t)) (union (union y (union x z)) t).
 Proof.
-Intros; Apply seq_trans with (union (union x (union y z)) t).
-Apply seq_sym; Apply union_ass.
-Apply seq_left; Apply union_perm_left.
+intros; apply seq_trans with (union (union x (union y z)) t).
+apply seq_sym; apply union_ass.
+apply seq_left; apply union_perm_left.
 Qed.
 
 (** specific for treesort *)
 
-Lemma treesort_twist1 : (x,y,z,t,u:uniset) (seq u (union y z)) ->
-   (seq (union x (union u t)) (union (union y (union x t)) z)).
+Lemma treesort_twist1 :
+ forall x y z t u:uniset,
+   seq u (union y z) ->
+   seq (union x (union u t)) (union (union y (union x t)) z).
 Proof.
-Intros; Apply seq_trans with (union x (union (union y z) t)).
-Apply seq_right; Apply seq_left; Trivial.
-Apply uniset_twist1.
+intros; apply seq_trans with (union x (union (union y z) t)).
+apply seq_right; apply seq_left; trivial.
+apply uniset_twist1.
 Qed.
 
-Lemma treesort_twist2 : (x,y,z,t,u:uniset) (seq u (union y z)) ->
-   (seq (union x (union u t)) (union (union y (union x z)) t)).
+Lemma treesort_twist2 :
+ forall x y z t u:uniset,
+   seq u (union y z) ->
+   seq (union x (union u t)) (union (union y (union x z)) t).
 Proof.
-Intros; Apply seq_trans with (union x (union (union y z) t)).
-Apply seq_right; Apply seq_left; Trivial.
-Apply uniset_twist2.
+intros; apply seq_trans with (union x (union (union y z) t)).
+apply seq_right; apply seq_left; trivial.
+apply uniset_twist2.
 Qed.
 
 
@@ -209,4 +212,4 @@ i*)
 
 End defs.
 
-Unset Implicit Arguments.
+Unset Implicit Arguments.
\ No newline at end of file