Réparation de FSet (back to 8628)

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

1 files changed, 246 insertions, 246 deletions

diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 0a13ee78e..bcd966f9a 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(* $Id: FSetWeakList.v,v 1.8 2006/03/09 18:34:51 letouzey Exp $ *)
 
 (** * Finite sets library *)
 
@@ -23,116 +23,116 @@ Unset Strict Implicit.
    The specs are proved under the additional condition of no redundancy. 
    And the functions returning sets are proved to preserve this invariant. *)
 
-Module Raw (X DecidableType).
+Module Raw (X: DecidableType).
  
-  Module E = X.
+  Module E := X.
 
-  Definition elt = X.t.
-  Definition t = list elt.
+  Definition elt := X.t.
+  Definition t := list elt.
 
-  Definition empty  t := nil.
+  Definition empty : t := nil.
 
-  Definition is_empty (l  t) : bool := if l then true else false.
+  Definition is_empty (l : t) : bool := if l then true else false.
 
   (** ** The set operations. *)
 
-  Fixpoint mem (x  elt) (s : t) {struct s} : bool :=
+  Fixpoint mem (x : elt) (s : t) {struct s} : bool :=
     match s with
     | nil => false
-    | y : l =>
+    | y :: l =>
            if X.eq_dec x y then true else mem x l
     end.
 
-  Fixpoint add (x  elt) (s : t) {struct s} : t :=
+  Fixpoint add (x : elt) (s : t) {struct s} : t :=
     match s with
-    | nil => x : nil
-    | y : l =>
-        if X.eq_dec x y then s else y : add x l
+    | nil => x :: nil
+    | y :: l =>
+        if X.eq_dec x y then s else y :: add x l
     end.
 
-  Definition singleton (x  elt) : t := x :: nil. 
+  Definition singleton (x : elt) : t := x :: nil. 
 
-  Fixpoint remove (x  elt) (s : t) {struct s} : t :=
+  Fixpoint remove (x : elt) (s : t) {struct s} : t :=
     match s with
     | nil => nil
-    | y : l =>
-        if X.eq_dec x y then l else y : remove x l
+    | y :: l =>
+        if X.eq_dec x y then l else y :: remove x l
     end.
 
-  Fixpoint fold (B  Set) (f : elt -> B -> B) (s : t) {struct s} : 
-   B -> B = fun i => match s with
+  Fixpoint fold (B : Set) (f : elt -> B -> B) (s : t) {struct s} : 
+   B -> B := fun i => match s with
                       | nil => i
-                      | x : l => fold f l (f x i)
+                      | x :: l => fold f l (f x i)
                       end.  
 
-  Definition union (s  t) : t -> t := fold add s.
+  Definition union (s : t) : t -> t := fold add s.
   
-  Definition diff (s s'  t) : t := fold remove s' s.
+  Definition diff (s s' : t) : t := fold remove s' s.
 
-  Definition inter (s s' t) : t := 
+  Definition inter (s s': t) : t := 
     fold (fun x s => if mem x s' then add x s else s) s nil.
 
-  Definition subset (s s'  t) : bool := is_empty (diff s s').
+  Definition subset (s s' : t) : bool := is_empty (diff s s').
 
-  Definition equal (s s'  t) : bool := andb (subset s s') (subset s' s). 
+  Definition equal (s s' : t) : bool := andb (subset s s') (subset s' s). 
 
-  Fixpoint filter (f  elt -> bool) (s : t) {struct s} : t :=
+  Fixpoint filter (f : elt -> bool) (s : t) {struct s} : t :=
     match s with
     | nil => nil
-    | x : l => if f x then x :: filter f l else filter f l
+    | x :: l => if f x then x :: filter f l else filter f l
     end.  
 
-  Fixpoint for_all (f  elt -> bool) (s : t) {struct s} : bool :=
+  Fixpoint for_all (f : elt -> bool) (s : t) {struct s} : bool :=
     match s with
     | nil => true
-    | x : l => if f x then for_all f l else false
+    | x :: l => if f x then for_all f l else false
     end.  
  
-  Fixpoint exists_ (f  elt -> bool) (s : t) {struct s} : bool :=
+  Fixpoint exists_ (f : elt -> bool) (s : t) {struct s} : bool :=
     match s with
     | nil => false
-    | x : l => if f x then true else exists_ f l
+    | x :: l => if f x then true else exists_ f l
     end.
 
-  Fixpoint partition (f  elt -> bool) (s : t) {struct s} : 
-   t * t =
+  Fixpoint partition (f : elt -> bool) (s : t) {struct s} : 
+   t * t :=
     match s with
     | nil => (nil, nil)
-    | x : l =>
-        let (s1, s2) = partition f l in
-        if f x then (x : s1, s2) else (s1, x :: s2)
+    | x :: l =>
+        let (s1, s2) := partition f l in
+        if f x then (x :: s1, s2) else (s1, x :: s2)
     end.
 
-  Definition cardinal (s  t) : nat := length s.
+  Definition cardinal (s : t) : nat := length s.
 
-  Definition elements (s  t) : list elt := s.
+  Definition elements (s : t) : list elt := s.
 
-  Definition choose (s  t) : option elt := 
+  Definition choose (s : t) : option elt := 
      match s with 
       | nil => None
-      | x:_ => Some x
+      | x::_ => Some x
      end.
 
   (** ** Proofs of set operation specifications. *)
 
-  Notation NoRedun = (noredunA X.eq).
-  Notation In = (InA X.eq).
+  Notation NoRedun := (noredunA X.eq).
+  Notation In := (InA X.eq).
 
-  Definition Equal s s' = forall a : elt, In a s <-> In a s'.
-  Definition Subset s s' = forall a : elt, In a s -> In a s'.
-  Definition Empty s = forall a : elt, ~ In a s.
-  Definition For_all (P  elt -> Prop) s := forall x, In x s -> P x.
-  Definition Exists (P  elt -> Prop) s := exists x, In x s /\ P x.
+  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
+  Definition Subset s s' := forall a : elt, In a s -> In a s'.
+  Definition Empty s := forall a : elt, ~ In a s.
+  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
+  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
 
-  Lemma In_eq 
-    forall (s  t) (x y : elt), X.eq x y -> In x s -> In y s.
+  Lemma In_eq :
+    forall (s : t) (x y : elt), X.eq x y -> In x s -> In y s.
   Proof.
   intros s x y; do 2 setoid_rewrite InA_alt; firstorder eauto.
   Qed.
   Hint Immediate In_eq.
 
-  Lemma mem_1 
-   forall (s  t)(x : elt), In x s -> mem x s = true. 
+  Lemma mem_1 :
+   forall (s : t)(x : elt), In x s -> mem x s = true. 
   Proof.
   induction s; intros.
   inversion H.
@@ -140,7 +140,7 @@ Module Raw (X DecidableType).
   inversion_clear H; auto.
   Qed.
 
-  Lemma mem_2  forall (s : t) (x : elt), mem x s = true -> In x s.
+  Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s.
   Proof.
   induction s. 
   intros; inversion H.
@@ -148,8 +148,8 @@ Module Raw (X DecidableType).
   destruct (X.eq_dec x a); firstorder; discriminate.
   Qed.
 
-  Lemma add_1 
-   forall (s  t) (Hs : NoRedun s) (x y : elt), X.eq x y -> In y (add x s).
+  Lemma add_1 :
+   forall (s : t) (Hs : NoRedun s) (x y : elt), X.eq x y -> In y (add x s).
   Proof.
   induction s. 
   simpl; intuition.
@@ -158,8 +158,8 @@ Module Raw (X DecidableType).
   eauto.
   Qed.
 
-  Lemma add_2 
-   forall (s  t) (Hs : NoRedun s) (x y : elt), In y s -> In y (add x s).
+  Lemma add_2 :
+   forall (s : t) (Hs : NoRedun s) (x y : elt), In y s -> In y (add x s).
   Proof.
   induction s. 
   simpl; intuition.
@@ -167,8 +167,8 @@ Module Raw (X DecidableType).
   inversion_clear Hs; eauto; inversion_clear H; intuition.
   Qed.
 
-  Lemma add_3 
-   forall (s  t) (Hs : NoRedun s) (x y : elt),
+  Lemma add_3 :
+   forall (s : t) (Hs : NoRedun s) (x y : elt),
    ~ X.eq x y -> In y (add x s) -> In y s.
   Proof.
   induction s. 
@@ -179,8 +179,8 @@ Module Raw (X DecidableType).
    absurd (X.eq x y); auto.
   Qed.
 
-  Lemma add_unique 
-   forall (s  t) (Hs : NoRedun s)(x:elt), NoRedun (add x s).
+  Lemma add_unique :
+   forall (s : t) (Hs : NoRedun s)(x:elt), NoRedun (add x s).
   Proof.
   induction s.  
   simpl; intuition.
@@ -196,8 +196,8 @@ Module Raw (X DecidableType).
   eapply add_3; eauto.
   Qed.
 
-  Lemma remove_1 
-   forall (s  t) (Hs : NoRedun s) (x y : elt), X.eq x y -> ~ In y (remove x s).
+  Lemma remove_1 :
+   forall (s : t) (Hs : NoRedun s) (x y : elt), X.eq x y -> ~ In y (remove x s).
   Proof.
   simple induction s. 
   simpl; red; intros; inversion H0.
@@ -207,8 +207,8 @@ Module Raw (X DecidableType).
   inversion_clear H1; eauto.
   Qed.
 
-  Lemma remove_2 
-   forall (s  t) (Hs : NoRedun s) (x y : elt),
+  Lemma remove_2 :
+   forall (s : t) (Hs : NoRedun s) (x y : elt),
    ~ X.eq x y -> In y s -> In y (remove x s).
   Proof.
   simple induction s. 
@@ -218,8 +218,8 @@ Module Raw (X DecidableType).
   absurd (X.eq x y); eauto. 
   Qed.
 
-  Lemma remove_3 
-   forall (s  t) (Hs : NoRedun s) (x y : elt), In y (remove x s) -> In y s.
+  Lemma remove_3 :
+   forall (s : t) (Hs : NoRedun s) (x y : elt), In y (remove x s) -> In y s.
   Proof.
   simple induction s. 
   simpl; intuition.
@@ -227,8 +227,8 @@ Module Raw (X DecidableType).
   inversion_clear Hs; inversion_clear H; firstorder.
   Qed.
 
-  Lemma remove_unique 
-   forall (s  t) (Hs : NoRedun s) (x : elt), NoRedun (remove x s).
+  Lemma remove_unique :
+   forall (s : t) (Hs : NoRedun s) (x : elt), NoRedun (remove x s).
   Proof.
   simple induction s.
   simpl; intuition.
@@ -239,69 +239,69 @@ Module Raw (X DecidableType).
   eapply remove_3; eauto.
   Qed. 
 
-  Lemma singleton_unique  forall x : elt, NoRedun (singleton x).
+  Lemma singleton_unique : forall x : elt, NoRedun (singleton x).
   Proof.
   unfold singleton; simpl; constructor; auto; intro H; inversion H.
   Qed.
 
-  Lemma singleton_1  forall x y : elt, In y (singleton x) -> X.eq x y.
+  Lemma singleton_1 : forall x y : elt, In y (singleton x) -> X.eq x y.
   Proof.
   unfold singleton; simpl; intuition.
   inversion_clear H; auto; inversion H0.
   Qed. 
 
-  Lemma singleton_2  forall x y : elt, X.eq x y -> In y (singleton x).
+  Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x).
   Proof.
   unfold singleton; simpl; intuition.
   Qed. 
   
-  Lemma empty_unique  NoRedun empty.
+  Lemma empty_unique : NoRedun empty.
   Proof.
   unfold empty; constructor.
   Qed.
 
-  Lemma empty_1  Empty empty.
+  Lemma empty_1 : Empty empty.
   Proof.
   unfold Empty, empty; intuition; inversion H.
   Qed. 
 
-  Lemma is_empty_1  forall s : t, Empty s -> is_empty s = true.
+  Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true.
   Proof.
   unfold Empty; intro s; case s; simpl; intuition.
   elim (H e); auto.
   Qed.
   
-  Lemma is_empty_2  forall s : t, is_empty s = true -> Empty s. 
+  Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s. 
   Proof.
   unfold Empty; intro s; case s; simpl; intuition;
    inversion H0.
   Qed.
 
-  Lemma elements_1  forall (s : t) (x : elt), In x s -> In x (elements s).
+  Lemma elements_1 : forall (s : t) (x : elt), In x s -> In x (elements s).
   Proof.
   unfold elements; auto.
   Qed.
 
-  Lemma elements_2  forall (s : t) (x : elt), In x (elements s) -> In x s.
+  Lemma elements_2 : forall (s : t) (x : elt), In x (elements s) -> In x s.
   Proof. 
   unfold elements; auto.
   Qed.
  
-  Lemma elements_3  forall (s : t) (Hs : NoRedun s), NoRedun (elements s).  
+  Lemma elements_3 : forall (s : t) (Hs : NoRedun s), NoRedun (elements s).  
   Proof. 
   unfold elements; auto.
   Qed.
 
-  Lemma fold_1 
-   forall (s  t) (Hs : NoRedun s) (A : Set) (i : A) (f : elt -> A -> A),
+  Lemma fold_1 :
+   forall (s : t) (Hs : NoRedun s) (A : Set) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof.
   induction s; simpl; auto; intros.
   inversion_clear Hs; auto.
   Qed.
 
-  Lemma union_unique 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (union s s').
+  Lemma union_unique :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (union s s').
   Proof.
   unfold union; induction s; simpl; auto; intros.
   inversion_clear Hs.
@@ -309,8 +309,8 @@ Module Raw (X DecidableType).
   apply add_unique; auto.
   Qed.
   
-  Lemma union_1 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma union_1 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x (union s s') -> In x s \/ In x s'.
   Proof.
   unfold union; induction s; simpl; auto; intros.
@@ -321,8 +321,8 @@ Module Raw (X DecidableType).
   right; eapply add_3; eauto.
   Qed.
 
-  Lemma union_0  
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma union_0 : 
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x s \/ In x s' -> In x (union s s').
   Proof.
   unfold union; induction s; simpl; auto; intros.
@@ -337,25 +337,25 @@ Module Raw (X DecidableType).
   right; apply add_2; auto.
   Qed.
 
-  Lemma union_2 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma union_2 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x s -> In x (union s s').
   Proof.
   intros; apply union_0; auto.
   Qed.
 
-  Lemma union_3 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma union_3 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x s' -> In x (union s s').
   Proof.
   intros; apply union_0; auto.
   Qed.
 
-  Lemma inter_unique 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (inter s s').
+  Lemma inter_unique :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (inter s s').
   Proof.
   unfold inter; intros s.
-  set (acc = nil (A:=elt)).
+  set (acc := nil (A:=elt)).
   assert (NoRedun acc) by (unfold acc; auto).
   clearbody acc; generalize H; clear H; generalize acc; clear acc. 
   induction s; simpl; auto; intros.
@@ -365,12 +365,12 @@ Module Raw (X DecidableType).
   apply add_unique; auto.
   Qed.  
   
-  Lemma inter_0  
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma inter_0  :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x (inter s s') -> In x s /\ In x s'.
   Proof.
   unfold inter; intros.
-  set (acc = nil (A:=elt)) in *.
+  set (acc := nil (A:=elt)) in *.
   assert (NoRedun acc) by (unfold acc; auto).
   cut ((In x s /\ In x s') \/ In x acc).
     destruct 1; auto.
@@ -392,29 +392,29 @@ Module Raw (X DecidableType).
   left; intuition.
   Qed.
 
-  Lemma inter_1  
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma inter_1  :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x (inter s s') -> In x s.
   Proof.
   intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ].
   Qed.
 
-  Lemma inter_2 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma inter_2 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x (inter s s') -> In x s'.
   Proof.
   intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ].
   Qed.
 
-  Lemma inter_3 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma inter_3 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x s -> In x s' -> In x (inter s s').
   Proof.
   intros s s' Hs Hs' x.
-  cut (((In x s /\ In x s')\/ In x (nil (A=elt))) -> In x (inter s s')).
+  cut (((In x s /\ In x s')\/ In x (nil (A:=elt))) -> In x (inter s s')).
   intuition.
   unfold inter.
-  set (acc = nil (A:=elt)) in *.
+  set (acc := nil (A:=elt)) in *.
   assert (NoRedun acc) by (unfold acc; auto).
   clearbody acc. 
   generalize H Hs' Hs; clear H Hs Hs'.
@@ -440,8 +440,8 @@ Module Raw (X DecidableType).
   discriminate.
   Qed.
 
-  Lemma diff_unique 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (diff s s').
+  Lemma diff_unique :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (diff s s').
   Proof.
   unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
   induction s'; simpl; auto; intros.
@@ -450,8 +450,8 @@ Module Raw (X DecidableType).
   apply remove_unique; auto.
   Qed.  
   
-  Lemma diff_0 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma diff_0 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x (diff s s') -> In x s /\ ~ In x s'.
   Proof.
   unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
@@ -467,22 +467,22 @@ Module Raw (X DecidableType).
   destruct (remove_1 Hs (X.eq_sym H5) H2).
   Qed.
 
-  Lemma diff_1 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma diff_1 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x (diff s s') -> In x s.
   Proof.
   intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto]. 
   Qed.
 
-  Lemma diff_2 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma diff_2 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x (diff s s') -> ~ In x s'.
   Proof.
   intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto]. 
   Qed.
 
-  Lemma diff_3 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+  Lemma diff_3 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
    In x s -> ~ In x s' -> In x (diff s s').
   Proof.
   unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
@@ -493,8 +493,8 @@ Module Raw (X DecidableType).
   apply remove_2; auto.
   Qed.  
   
-  Lemma subset_1 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s'),
+  Lemma subset_1 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'),
    Subset s s' -> subset s s' = true.
   Proof.
   unfold subset, Subset; intros.
@@ -506,7 +506,7 @@ Module Raw (X DecidableType).
   eapply diff_1; eauto.
   Qed.
 
-  Lemma subset_2  forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'), 
+  Lemma subset_2 : forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'), 
      subset s s' = true -> Subset s s'.
   Proof.
   unfold subset, Subset; intros.
@@ -518,15 +518,15 @@ Module Raw (X DecidableType).
   apply diff_3; intuition.
   Qed.
 
-  Lemma equal_1 
-   forall (s s'  t) (Hs : NoRedun s) (Hs' : NoRedun s'),
+  Lemma equal_1 :
+   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'),
    Equal s s' -> equal s s' = true.
   Proof.
   unfold Equal, equal; intros.
   apply andb_true_intro; split; apply subset_1; firstorder.
   Qed.
 
-  Lemma equal_2  forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'),  
+  Lemma equal_2 : forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'),  
      equal s s' = true -> Equal s s'.
   Proof.
   unfold Equal, equal; intros.
@@ -534,27 +534,27 @@ Module Raw (X DecidableType).
   split; apply subset_2; auto.
   Qed.  
 
-  Definition choose_1 
-    forall (s  t) (x : elt), choose s = Some x -> In x s.
+  Definition choose_1 :
+    forall (s : t) (x : elt), choose s = Some x -> In x s.
   Proof.
   destruct s; simpl; intros; inversion H; auto.
   Qed.  
 
-  Definition choose_2  forall s : t, choose s = None -> Empty s.
+  Definition choose_2 : forall s : t, choose s = None -> Empty s.
   Proof.
   destruct s; simpl; intros.
   intros x H0; inversion H0.
   inversion H.
   Qed.  
 
-  Lemma cardinal_1 
-   forall (s  t) (Hs : NoRedun s), cardinal s = length (elements s).
+  Lemma cardinal_1 :
+   forall (s : t) (Hs : NoRedun s), cardinal s = length (elements s).
   Proof.
   auto.
   Qed.
 
-  Lemma filter_1 
-   forall (s  t) (x : elt) (f : elt -> bool),
+  Lemma filter_1 :
+   forall (s : t) (x : elt) (f : elt -> bool),
    In x (filter f s) -> In x s.
   Proof.
   simple induction s; simpl.
@@ -567,8 +567,8 @@ Module Raw (X DecidableType).
   constructor 2; apply (Hrec a f); trivial.
   Qed.
 
-   Lemma filter_2 
-    forall (s  t) (x : elt) (f : elt -> bool),
+   Lemma filter_2 :
+    forall (s : t) (x : elt) (f : elt -> bool),
     compat_bool X.eq f -> In x (filter f s) -> f x = true.   
    Proof.
   simple induction s; simpl.
@@ -579,8 +579,8 @@ Module Raw (X DecidableType).
   symmetry; auto.
   Qed.
  
-  Lemma filter_3 
-   forall (s  t) (x : elt) (f : elt -> bool),
+  Lemma filter_3 :
+   forall (s : t) (x : elt) (f : elt -> bool),
    compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).     
   Proof.
   simple induction s; simpl.
@@ -592,8 +592,8 @@ Module Raw (X DecidableType).
   rewrite <- (H a (X.eq_sym H1)); intros; discriminate.
   Qed.
 
-  Lemma filter_unique 
-   forall (s  t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (filter f s).
+  Lemma filter_unique :
+   forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (filter f s).
   Proof.
   simple induction s; simpl.
   auto.
@@ -605,8 +605,8 @@ Module Raw (X DecidableType).
   Qed.
 
 
-  Lemma for_all_1 
-   forall (s  t) (f : elt -> bool),
+  Lemma for_all_1 :
+   forall (s : t) (f : elt -> bool),
    compat_bool X.eq f ->
    For_all (fun x => f x = true) s -> for_all f s = true.
   Proof. 
@@ -617,8 +617,8 @@ Module Raw (X DecidableType).
   intros; rewrite (H x); auto.
   Qed.
 
-  Lemma for_all_2 
-   forall (s  t) (f : elt -> bool),
+  Lemma for_all_2 :
+   forall (s : t) (f : elt -> bool),
    compat_bool X.eq f ->
    for_all f s = true -> For_all (fun x => f x = true) s.
   Proof. 
@@ -633,8 +633,8 @@ Module Raw (X DecidableType).
   rewrite (Hf a x); auto.
   Qed.
 
-  Lemma exists_1 
-   forall (s  t) (f : elt -> bool),
+  Lemma exists_1 :
+   forall (s : t) (f : elt -> bool),
    compat_bool X.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
   Proof.
   simple induction s; simpl; auto; unfold Exists.
@@ -651,8 +651,8 @@ Module Raw (X DecidableType).
   exists a; auto.
   Qed.
 
-  Lemma exists_2 
-   forall (s  t) (f : elt -> bool),
+  Lemma exists_2 :
+   forall (s : t) (f : elt -> bool),
    compat_bool X.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
   Proof. 
   simple induction s; simpl; auto; unfold Exists.
@@ -664,8 +664,8 @@ Module Raw (X DecidableType).
   exists a; auto.
   Qed.
 
-  Lemma partition_1 
-   forall (s  t) (f : elt -> bool),
+  Lemma partition_1 :
+   forall (s : t) (f : elt -> bool),
    compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s).
   Proof.
   simple induction s; simpl; auto; unfold Equal.
@@ -676,8 +676,8 @@ Module Raw (X DecidableType).
   case (f x); simpl; firstorder; inversion H0; intros; firstorder. 
   Qed.
    
-  Lemma partition_2 
-   forall (s  t) (f : elt -> bool),
+  Lemma partition_2 :
+   forall (s : t) (f : elt -> bool),
    compat_bool X.eq f ->
    Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
   Proof.
@@ -689,8 +689,8 @@ Module Raw (X DecidableType).
   case (f x); simpl; firstorder; inversion H0; intros; firstorder. 
   Qed.
 
-  Lemma partition_aux_1  
-   forall (s  t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), 
+  Lemma partition_aux_1 : 
+   forall (s : t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), 
     In x (fst (partition f s)) -> In x s.
   Proof.
   induction s; simpl; auto; intros.
@@ -700,8 +700,8 @@ Module Raw (X DecidableType).
   inversion_clear H; auto.
   Qed. 
      
-  Lemma partition_aux_2  
-   forall (s  t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), 
+  Lemma partition_aux_2 : 
+   forall (s : t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), 
     In x (snd (partition f s)) -> In x s.
   Proof.
   induction s; simpl; auto; intros.
@@ -711,8 +711,8 @@ Module Raw (X DecidableType).
   inversion_clear H; auto.
   Qed. 
   
-  Lemma partition_unique_1 
-   forall (s  t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (fst (partition f s)).
+  Lemma partition_unique_1 :
+   forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (fst (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.
@@ -722,8 +722,8 @@ Module Raw (X DecidableType).
   case (f x); case (partition f l); simpl; auto.
   Qed.
   
-  Lemma partition_unique_2 
-   forall (s  t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (snd (partition f s)).
+  Lemma partition_unique_2 :
+   forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (snd (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.
@@ -733,19 +733,19 @@ Module Raw (X DecidableType).
   case (f x); case (partition f l); simpl; auto.
   Qed.
  
-  Definition eq  t -> t -> Prop := Equal.
+  Definition eq : t -> t -> Prop := Equal.
 
-  Lemma eq_refl  forall s : t, eq s s. 
+  Lemma eq_refl : forall s : t, eq s s. 
   Proof. 
   unfold eq, Equal; intuition.
   Qed.
 
-  Lemma eq_sym  forall s s' : t, eq s s' -> eq s' s.
+  Lemma eq_sym : forall s s' : t, eq s s' -> eq s' s.
   Proof. 
   unfold eq, Equal; firstorder.
   Qed.
 
-  Lemma eq_trans  forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
+  Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
   Proof. 
   unfold eq, Equal; firstorder.
   Qed.
@@ -757,117 +757,117 @@ End Raw.
    Now, in order to really provide a functor implementing [S], we 
    need to encapsulate everything into a type of lists without redundancy. *)
 
-Module Make (X DecidableType) <: S with Module E := X.
+Module Make (X: DecidableType) <: S with Module E := X.
 
- Module E = X.
- Module Raw = Raw X. 
+ Module E := X.
+ Module Raw := Raw X. 
 
- Record slist  Set :=  {this :> Raw.t; unique : noredunA X.eq this}.
- Definition t = slist. 
- Definition elt = X.t.
+ Record slist : Set :=  {this :> Raw.t; unique : noredunA X.eq this}.
+ Definition t := slist. 
+ Definition elt := X.t.
  
- Definition In (x  elt) (s : t) := InA X.eq x s.(this).
- Definition Equal s s' = forall a : elt, In a s <-> In a s'.
- Definition Subset s s' = forall a : elt, In a s -> In a s'.
- Definition Empty s = forall a : elt, ~ In a s.
- Definition For_all (P  elt -> Prop) (s : t) :=
-   forall x  elt, In x s -> P x.
- Definition Exists (P  elt -> Prop) (s : t) := exists x : elt, In x s /\ P x.
+ Definition In (x : elt) (s : t) := InA X.eq x s.(this).
+ Definition Equal s s' := forall a : elt, In a s <-> In a s'.
+ Definition Subset s s' := forall a : elt, In a s -> In a s'.
+ Definition Empty s := forall a : elt, ~ In a s.
+ Definition For_all (P : elt -> Prop) (s : t) :=
+   forall x : elt, In x s -> P x.
+ Definition Exists (P : elt -> Prop) (s : t) := exists x : elt, In x s /\ P x.
   
- Definition In_1 (s  t) := Raw.In_eq (s:=s).
+ Definition In_1 (s : t) := Raw.In_eq (s:=s).
  
- Definition mem (x  elt) (s : t) := Raw.mem x s.
- Definition mem_1 (s  t) := Raw.mem_1 (s:=s). 
- Definition mem_2 (s  t) := Raw.mem_2 (s:=s).
-
- Definition add x s = Build_slist (Raw.add_unique (unique s) x).
- Definition add_1 (s  t) := Raw.add_1 (unique s).
- Definition add_2 (s  t) := Raw.add_2 (unique s).
- Definition add_3 (s  t) := Raw.add_3 (unique s).
-
- Definition remove x s = Build_slist (Raw.remove_unique (unique s) x).
- Definition remove_1 (s  t) := Raw.remove_1 (unique s).
- Definition remove_2 (s  t) := Raw.remove_2 (unique s).
- Definition remove_3 (s  t) := Raw.remove_3 (unique s).
+ Definition mem (x : elt) (s : t) := Raw.mem x s.
+ Definition mem_1 (s : t) := Raw.mem_1 (s:=s). 
+ Definition mem_2 (s : t) := Raw.mem_2 (s:=s).
+
+ Definition add x s := Build_slist (Raw.add_unique (unique s) x).
+ Definition add_1 (s : t) := Raw.add_1 (unique s).
+ Definition add_2 (s : t) := Raw.add_2 (unique s).
+ Definition add_3 (s : t) := Raw.add_3 (unique s).
+
+ Definition remove x s := Build_slist (Raw.remove_unique (unique s) x).
+ Definition remove_1 (s : t) := Raw.remove_1 (unique s).
+ Definition remove_2 (s : t) := Raw.remove_2 (unique s).
+ Definition remove_3 (s : t) := Raw.remove_3 (unique s).
  
- Definition singleton x = Build_slist (Raw.singleton_unique x).
- Definition singleton_1 = Raw.singleton_1.
- Definition singleton_2 = Raw.singleton_2.
+ Definition singleton x := Build_slist (Raw.singleton_unique x).
+ Definition singleton_1 := Raw.singleton_1.
+ Definition singleton_2 := Raw.singleton_2.
   
- Definition union (s s'  t) :=
+ Definition union (s s' : t) :=
    Build_slist (Raw.union_unique (unique s) (unique s')). 
- Definition union_1 (s s'  t) := Raw.union_1 (unique s) (unique s').
- Definition union_2 (s s'  t) := Raw.union_2 (unique s) (unique s').
- Definition union_3 (s s'  t) := Raw.union_3 (unique s) (unique s').
+ Definition union_1 (s s' : t) := Raw.union_1 (unique s) (unique s').
+ Definition union_2 (s s' : t) := Raw.union_2 (unique s) (unique s').
+ Definition union_3 (s s' : t) := Raw.union_3 (unique s) (unique s').
 
- Definition inter (s s'  t) :=
+ Definition inter (s s' : t) :=
    Build_slist (Raw.inter_unique (unique s) (unique s')). 
- Definition inter_1 (s s'  t) := Raw.inter_1 (unique s) (unique s').
- Definition inter_2 (s s'  t) := Raw.inter_2 (unique s) (unique s').
- Definition inter_3 (s s'  t) := Raw.inter_3 (unique s) (unique s').
+ Definition inter_1 (s s' : t) := Raw.inter_1 (unique s) (unique s').
+ Definition inter_2 (s s' : t) := Raw.inter_2 (unique s) (unique s').
+ Definition inter_3 (s s' : t) := Raw.inter_3 (unique s) (unique s').
  
- Definition diff (s s'  t) :=
+ Definition diff (s s' : t) :=
    Build_slist (Raw.diff_unique (unique s) (unique s')). 
- Definition diff_1 (s s'  t) := Raw.diff_1 (unique s) (unique s').
- Definition diff_2 (s s'  t) := Raw.diff_2 (unique s) (unique s').
- Definition diff_3 (s s'  t) := Raw.diff_3 (unique s) (unique s').
+ Definition diff_1 (s s' : t) := Raw.diff_1 (unique s) (unique s').
+ Definition diff_2 (s s' : t) := Raw.diff_2 (unique s) (unique s').
+ Definition diff_3 (s s' : t) := Raw.diff_3 (unique s) (unique s').
  
- Definition equal (s s'  t) := Raw.equal s s'. 
- Definition equal_1 (s s'  t) := Raw.equal_1 (unique s) (unique s').  
- Definition equal_2 (s s'  t) := Raw.equal_2 (unique s) (unique s').
+ Definition equal (s s' : t) := Raw.equal s s'. 
+ Definition equal_1 (s s' : t) := Raw.equal_1 (unique s) (unique s').  
+ Definition equal_2 (s s' : t) := Raw.equal_2 (unique s) (unique s').
  
- Definition subset (s s'  t) := Raw.subset s s'.
- Definition subset_1 (s s'  t) := Raw.subset_1 (unique s) (unique s').  
- Definition subset_2 (s s'  t) := Raw.subset_2 (unique s) (unique s').
+ Definition subset (s s' : t) := Raw.subset s s'.
+ Definition subset_1 (s s' : t) := Raw.subset_1 (unique s) (unique s').  
+ Definition subset_2 (s s' : t) := Raw.subset_2 (unique s) (unique s').
 
- Definition empty = Build_slist Raw.empty_unique.
- Definition empty_1 = Raw.empty_1.
+ Definition empty := Build_slist Raw.empty_unique.
+ Definition empty_1 := Raw.empty_1.
  
- Definition is_empty (s  t) := Raw.is_empty s.
- Definition is_empty_1 (s  t) := Raw.is_empty_1 (s:=s).
- Definition is_empty_2 (s  t) := Raw.is_empty_2 (s:=s).
-
- Definition elements (s  t) := Raw.elements s.
- Definition elements_1 (s  t) := Raw.elements_1 (s:=s).
- Definition elements_2 (s  t) := Raw.elements_2 (s:=s).
- Definition elements_3 (s  t) := Raw.elements_3 (unique s).
+ Definition is_empty (s : t) := Raw.is_empty s.
+ Definition is_empty_1 (s : t) := Raw.is_empty_1 (s:=s).
+ Definition is_empty_2 (s : t) := Raw.is_empty_2 (s:=s).
+
+ Definition elements (s : t) := Raw.elements s.
+ Definition elements_1 (s : t) := Raw.elements_1 (s:=s).
+ Definition elements_2 (s : t) := Raw.elements_2 (s:=s).
+ Definition elements_3 (s : t) := Raw.elements_3 (unique s).
   
- Definition choose (st) := Raw.choose s.
- Definition choose_1 (s  t) := Raw.choose_1 (s:=s).
- Definition choose_2 (s  t) := Raw.choose_2 (s:=s).
+ Definition choose (s:t) := Raw.choose s.
+ Definition choose_1 (s : t) := Raw.choose_1 (s:=s).
+ Definition choose_2 (s : t) := Raw.choose_2 (s:=s).
   
- Definition fold (B  Set) (f : elt -> B -> B) (s : t) := Raw.fold (B:=B) f s. 
- Definition fold_1 (s  t) := Raw.fold_1 (unique s). 
+ Definition fold (B : Set) (f : elt -> B -> B) (s : t) := Raw.fold (B:=B) f s. 
+ Definition fold_1 (s : t) := Raw.fold_1 (unique s). 
  
- Definition cardinal (s  t) := Raw.cardinal s.
- Definition cardinal_1 (s  t) := Raw.cardinal_1 (unique s). 
+ Definition cardinal (s : t) := Raw.cardinal s.
+ Definition cardinal_1 (s : t) := Raw.cardinal_1 (unique s). 
  
- Definition filter (f  elt -> bool) (s : t) :=
+ Definition filter (f : elt -> bool) (s : t) :=
    Build_slist (Raw.filter_unique (unique s) f).
- Definition filter_1 (s  t)(x:elt)(f: elt -> bool)(H:compat_bool X.eq f) := 
+ Definition filter_1 (s : t)(x:elt)(f: elt -> bool)(H:compat_bool X.eq f) := 
     @Raw.filter_1 s x f.
- Definition filter_2 (s  t) := Raw.filter_2 (s:=s).
- Definition filter_3 (s  t) := Raw.filter_3 (s:=s).
+ Definition filter_2 (s : t) := Raw.filter_2 (s:=s).
+ Definition filter_3 (s : t) := Raw.filter_3 (s:=s).
  
- Definition for_all (f  elt -> bool) (s : t) := Raw.for_all f s.
- Definition for_all_1 (s  t) := Raw.for_all_1 (s:=s). 
- Definition for_all_2 (s  t) := Raw.for_all_2 (s:=s). 
-
- Definition exists_ (f  elt -> bool) (s : t) := Raw.exists_ f s.
- Definition exists_1 (s  t) := Raw.exists_1 (s:=s). 
- Definition exists_2 (s  t) := Raw.exists_2 (s:=s). 
-
- Definition partition (f  elt -> bool) (s : t) :=
-   let p = Raw.partition f s in
-   (Build_slist (this=fst p) (Raw.partition_unique_1 (unique s) f),
-   Build_slist (this=snd p) (Raw.partition_unique_2 (unique s) f)).
- Definition partition_1 (s  t) := Raw.partition_1 s.
- Definition partition_2 (s  t) := Raw.partition_2 s. 
-
- Definition eq (s s'  t) := Raw.eq s s'.
- Definition eq_refl (s  t) := Raw.eq_refl s.
- Definition eq_sym (s s'  t) := Raw.eq_sym (s:=s) (s':=s').
- Definition eq_trans (s s' s''  t) :=
-   Raw.eq_trans (s=s) (s':=s') (s'':=s'').
+ Definition for_all (f : elt -> bool) (s : t) := Raw.for_all f s.
+ Definition for_all_1 (s : t) := Raw.for_all_1 (s:=s). 
+ Definition for_all_2 (s : t) := Raw.for_all_2 (s:=s). 
+
+ Definition exists_ (f : elt -> bool) (s : t) := Raw.exists_ f s.
+ Definition exists_1 (s : t) := Raw.exists_1 (s:=s). 
+ Definition exists_2 (s : t) := Raw.exists_2 (s:=s). 
+
+ Definition partition (f : elt -> bool) (s : t) :=
+   let p := Raw.partition f s in
+   (Build_slist (this:=fst p) (Raw.partition_unique_1 (unique s) f),
+   Build_slist (this:=snd p) (Raw.partition_unique_2 (unique s) f)).
+ Definition partition_1 (s : t) := Raw.partition_1 s.
+ Definition partition_2 (s : t) := Raw.partition_2 s. 
+
+ Definition eq (s s' : t) := Raw.eq s s'.
+ Definition eq_refl (s : t) := Raw.eq_refl s.
+ Definition eq_sym (s s' : t) := Raw.eq_sym (s:=s) (s':=s').
+ Definition eq_trans (s s' s'' : t) :=
+   Raw.eq_trans (s:=s) (s':=s') (s'':=s'').
 
 End Make.