Reorganization of FSet+FMap : no more files specific to Weak Sets/Maps

Thanks to Elie's work and especially "Include Type ...", full sets can
be simply expressed as extensions of weak sets. Moreover, Facts and
Properties functors can be factorized almost completely. As a result,
things like FSetWeakAAA.BBB can now be found as FSetAAA.WBBB,

Same with maps / weak maps ...

No backward compatibility intended for weak sets / maps, but porting
scripts should mostly amounts to name changes (see above). 




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

21 files changed, 2634 insertions, 3740 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index f696ff075..3a3698239 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -15,18 +15,17 @@
   different styles: equivalence and boolean equalities. 
 *)
 
-Require Import Bool.
-Require Import OrderedType.
+Require Import Bool DecidableType DecidableTypeEx OrderedType.
 Require Export FMapInterface. 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Facts (M: S).
-Module ME := OrderedTypeFacts M.E.
-Import ME.
-Import M.
-Import Logic. (* to unmask [eq] *)  
-Import Peano. (* to unmask [lt] *)
+(** * Facts about weak maps *)
+
+Module WFacts (E:DecidableType)(Import M:WSfun E).
+
+Notation eq_dec := E.eq_dec.
+Definition eqb x y := if eq_dec x y then true else false.
 
 Lemma MapsTo_fun : forall (elt:Set) m x (e e':elt), 
   MapsTo x e m -> MapsTo x e' m -> e=e'.
@@ -36,7 +35,7 @@ generalize (find_1 H) (find_1 H0); clear H H0.
 intros; rewrite H in H0; injection H0; auto.
 Qed.
 
-(** * Specifications written using equivalences *)
+(** ** Specifications written using equivalences *)
 
 Section IffSpec. 
 Variable elt elt' elt'': Set.
@@ -230,7 +229,7 @@ destruct (mapi_1 f H) as (y,(H0,H1)).
 exists (f y a); auto.
 Qed.
 
-(* Unfortunately, we don't have simple equivalences for [mapi] 
+(** Unfortunately, we don't have simple equivalences for [mapi] 
   and [MapsTo]. The only correct one needs compatibility of [f]. *) 
 
 Lemma mapi_inv : forall m x b (f : key -> elt -> elt'), 
@@ -287,7 +286,7 @@ Ltac map_iff :=
   rewrite map_mapsto_iff || rewrite map_in_iff ||
   rewrite mapi_in_iff)).
 
-(**  * Specifications written using boolean predicates *)
+(** ** Specifications written using boolean predicates *)
 
 Section BoolSpec.
 
@@ -494,7 +493,7 @@ Proof.
 intros.
 case_eq (find x m); intros.
 rewrite <- H0.
-apply map2_1; auto.
+apply map2_1; auto with map.
 left; exists e; auto with map.
 case_eq (find x m'); intros.
 rewrite <- H0; rewrite <- H1.
@@ -514,21 +513,18 @@ Proof.
 intros.
 assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)).
  intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff.
-assert (NoDupA (eq_key (elt:=elt)) (elements m)). 
- apply SortA_NoDupA with (lt_key (elt:=elt)); unfold eq_key, lt_key; intuition eauto.
- destruct y; simpl in *.
- apply (E.lt_not_eq H0 H1).
- exact (elements_3 m).
+assert (H0:=elements_3w m).
 generalize (fun e => @findA_NoDupA _ _ _ E.eq_sym E.eq_trans eq_dec (elements m) x e H0).
-unfold eqb.
-destruct (find x m); destruct (findA (fun y : E.t => if eq_dec x y then true else false) (elements m)); 
+fold (eqb x).
+destruct (find x m); destruct (findA (eqb x) (elements m)); 
  simpl; auto; intros.
 symmetry; rewrite <- H1; rewrite <- H; auto.
 symmetry; rewrite <- H1; rewrite <- H; auto.
 rewrite H; rewrite H1; auto.
 Qed.
 
-Lemma elements_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (elements m).
+Lemma elements_b : forall m x, 
+ mem x m = existsb (fun p => eqb x (fst p)) (elements m).
 Proof.
 intros.
 generalize (mem_in_iff m x)(elements_in_iff m x)
@@ -554,31 +550,34 @@ Qed.
 
 End BoolSpec.
 
+End WFacts.
+
+(** * Same facts for full maps *)
+
+Module Facts (M:S). 
+ Module D := OT_as_DT M.E.
+ Include WFacts D M.
 End Facts.
 
-Module Properties (M: S).
- Module F:=Facts M. 
- Import F.
- Module O:=KeyOrderedType M.E.
- Import O.
+(** * Additional Properties for weak maps 
+ 
+    Results about [fold], [elements], induction principles...
+*)
+
+Module WProperties (E:DecidableType)(M:WSfun E).
+ Module Import F:=WFacts E M. 
  Import M.
 
  Section Elt. 
   Variable elt:Set.
 
-  Notation eqke := (@eqke elt).
-  Notation eqk := (@eqk elt).
-  Notation ltk := (@ltk elt).
-
   Definition cardinal (m:t elt) := length (elements m).
 
   Definition Equal (m m':t elt) := forall y, find y m = find y m'.
   Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).
 
-  Definition Above x (m:t elt) := forall y, In y m -> E.lt y x.
-  Definition Below x (m:t elt) := forall y, In y m -> E.lt x y.
-
-  Section Elements.
+  Notation eqke := (@eq_key_elt elt).
+  Notation eqk := (@eq_key elt).
 
   Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil.
   Proof.
@@ -599,6 +598,208 @@ Module Properties (M: S).
   rewrite H in H0; destruct H0 as (_,H0); inversion H0.
   Qed.
 
+  Lemma fold_Empty : forall m (A:Set)(f:key->elt->A->A)(i:A),
+   Empty m -> fold f m i = i.
+  Proof.
+  intros.
+  rewrite fold_1.
+  rewrite elements_Empty in H; rewrite H; simpl; auto.
+  Qed.
+
+  Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l.
+  Proof.
+  induction 1; auto.
+  constructor; auto.
+  contradict H.
+  destruct x as (x,y).
+  rewrite InA_alt in *; destruct H as ((a,b),((H1,H2),H3)); simpl in *.
+  exists (a,b); auto.
+  Qed.
+
+  Lemma fold_Equal : forall m1 m2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
+   (f:key->elt->A->A)(i:A), 
+   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
+   transpose eqA (fun y => f (fst y) (snd y)) -> 
+   Equal m1 m2 -> 
+   eqA (fold f m1 i) (fold f m2 i).
+  Proof.
+  assert (eqke_refl : forall p, eqke p p).
+   red; auto.
+  assert (eqke_sym : forall p p', eqke p p' -> eqke p' p).
+   intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition.
+  assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p'').
+   intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
+   intuition; eauto; congruence.
+  intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
+  apply fold_right_equivlistA with (eqA:=eqke) (eqB:=eqA); auto.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+  red; intros.
+  do 2 rewrite InA_rev.
+  destruct x; do 2 rewrite <- elements_mapsto_iff.
+  do 2 rewrite find_mapsto_iff.
+  rewrite H1; split; auto.
+  Qed.
+
+  Lemma fold_Add : forall m1 m2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
+   (f:key->elt->A->A)(i:A), 
+   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
+   transpose eqA (fun y =>f (fst y) (snd y)) -> 
+   ~In x m1 -> Add x e m1 m2 -> 
+   eqA (fold f m2 i) (f x e (fold f m1 i)).
+  Proof.
+  assert (eqke_refl : forall p, eqke p p).
+   red; auto.
+  assert (eqke_sym : forall p p', eqke p p' -> eqke p' p).
+   intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition.
+  assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p'').
+   intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
+   intuition; eauto; congruence.
+  intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
+  set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
+  change (f x e (fold_right f' i (rev (elements m1))))
+   with (f' (x,e) (fold_right f' i (rev (elements m1)))).
+  apply fold_right_add with (eqA:=eqke)(eqB:=eqA); auto.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+  rewrite InA_rev.
+  contradict H1.
+  exists e.
+  rewrite elements_mapsto_iff; auto.
+  intros a.
+  rewrite InA_cons; do 2 rewrite InA_rev; 
+  destruct a as (a,b); do 2 rewrite <- elements_mapsto_iff.
+  do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl.
+  rewrite H2.
+  rewrite add_o.
+  destruct (eq_dec x a); intuition.
+  inversion H3; auto.
+  f_equal; auto.
+  elim H1.
+  exists b; apply MapsTo_1 with a; auto with map.
+  elim n; auto.
+  Qed.
+
+  Lemma cardinal_fold : forall m, cardinal m = fold (fun _ _ => S) m 0.
+  Proof.
+  intros; unfold cardinal; rewrite fold_1.
+  symmetry; apply fold_left_length; auto.
+  Qed.
+
+  Lemma cardinal_Empty : forall m, Empty m <-> cardinal m = 0.
+  Proof.
+  intros.
+  rewrite elements_Empty.
+  unfold cardinal.
+  destruct (elements m); intuition; discriminate.
+  Qed.
+ 
+  Lemma Equal_cardinal : forall m m', Equal m m' -> cardinal m = cardinal m'.
+  Proof.
+  intros; do 2 rewrite cardinal_fold.
+  apply fold_Equal with (eqA:=@eq _); auto.
+  constructor; auto; congruence.
+  red; auto.
+  red; auto.
+  Qed.
+
+  Lemma cardinal_1 : forall m, Empty m -> cardinal m = 0.
+  Proof.
+  intros; rewrite <- cardinal_Empty; auto.
+  Qed.
+
+  Lemma cardinal_2 :
+    forall m m' x e, ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m).
+  Proof.
+  intros; do 2 rewrite cardinal_fold.
+  change S with ((fun _ _ => S) x e).
+  apply fold_Add; auto.
+  constructor; intros; auto; congruence.
+  red; simpl; auto.
+  red; simpl; auto.
+  Qed.
+
+  Lemma cardinal_inv_1 : forall m, cardinal m = 0 -> Empty m. 
+  Proof.
+  intros; rewrite cardinal_Empty; auto. 
+  Qed.
+  Hint Resolve cardinal_inv_1 : map.
+
+  Lemma cardinal_inv_2 :
+   forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
+  Proof. 
+  unfold cardinal; intros.
+  generalize (elements_mapsto_iff m).
+  destruct (elements m); try discriminate. 
+  exists p; auto.
+  rewrite H0; destruct p; simpl; auto.
+  constructor; red; auto.
+  Qed.
+
+  Lemma cardinal_inv_2b :
+   forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }.
+  Proof.
+  intros.
+  generalize (@cardinal_inv_2 m); destruct cardinal.
+  elim H;auto.
+  eauto.
+  Qed.
+
+  Lemma map_induction :
+   forall P : t elt -> Type,
+   (forall m, Empty m -> P m) ->
+   (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') ->
+   forall m, P m.
+  Proof.
+  intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.
+  apply X; apply cardinal_inv_1; auto.
+
+  destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *.
+  assert (Add x e (remove x m) m).
+   red; intros.
+   rewrite add_o; rewrite remove_o; destruct (eq_dec x y); eauto with map.
+  apply X0 with (remove x m) x e; auto with map.
+  apply IHn; auto with map.
+  assert (S n = S (cardinal (remove x m))).
+   rewrite Heqn; eapply cardinal_2; eauto with map.
+  inversion H1; auto with map.
+  Qed.
+
+ End Elt.
+
+End WProperties.
+
+(** * Same Properties for full maps *)
+
+Module Properties (M:S). 
+ Module D := OT_as_DT M.E.
+ Include WProperties D M.
+End Properties.
+
+(** * Properties specific to maps with ordered keys *)
+
+Module OrdProperties (M:S).
+ Module Import ME := OrderedTypeFacts M.E.
+ Module Import O:=KeyOrderedType M.E.
+ Module Import P:=Properties M.
+ Import F.
+ Import M.
+
+ Section Elt. 
+  Variable elt:Set.
+
+  Notation eqke := (@eqke elt).
+  Notation eqk := (@eqk elt).
+  Notation ltk := (@ltk elt).
+  Notation cardinal := (@cardinal elt).
+  Notation Equal := (@P.Equal elt).
+  Notation Add := (@Add elt).
+
+  Definition Above x (m:t elt) := forall y, In y m -> E.lt y x.
+  Definition Below x (m:t elt) := forall y, In y m -> E.lt x y.
+
+  Section Elements.
+
   Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt),
    sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'.
   Proof.
@@ -782,75 +983,6 @@ Module Properties (M: S).
 
   End Elements.
 
-  Section Cardinal.
-
-  Lemma cardinal_Empty : forall m, Empty m <-> cardinal m = 0.
-  Proof.
-   intros.
-   rewrite elements_Empty.
-   unfold cardinal.
-   destruct (elements m); intuition; discriminate.
-  Qed.
-
-  Lemma cardinal_inv_1 : forall (m:t elt), cardinal m = 0 -> Empty m. 
-  Proof. 
-    intros m; unfold cardinal; intros H e a.
-    rewrite elements_mapsto_iff.
-    destruct (elements m); simpl in *; discriminate || red; inversion 1.
-  Qed.
-
-  Lemma cardinal_inv_2 :
-   forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
-  Proof. 
-    intros; unfold cardinal in *.
-    generalize (elements_2 (m:=m)).
-    destruct (elements m); try discriminate. 
-    exists p; auto.
-    destruct p; simpl; auto.
-    apply H0; constructor; red; auto.
-  Qed.
-
-  Lemma cardinal_inv_2b :
-   forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }.
-  Proof. 
-    intros; unfold cardinal in *.
-    generalize (elements_2 (m:=m)).
-    destruct (elements m).
-    simpl in H; elim H; auto.
-    exists p; auto.
-    destruct p; simpl; auto.
-    apply H0; constructor; red; auto.
-  Qed.
-
-  Lemma cardinal_1 : forall (m:t elt), Empty m -> cardinal m = 0.
-  Proof.
-    intros; rewrite <- cardinal_Empty; auto.
-  Qed.
-
-  Lemma cardinal_2 : forall m m' x e, ~In x m -> Add x e m m' -> 
-    cardinal m' = S (cardinal m).
-  Proof.
-  intros.
-  unfold cardinal.
-  unfold key.
-  rewrite (eqlistA_length (elements_Add H H0)); simpl.
-  rewrite app_length; simpl.
-  rewrite <- plus_n_Sm.
-  f_equal.
-  rewrite <- app_length.
-  f_equal.
-  symmetry; apply elements_split; auto.
-  Qed.
-
-  Lemma cardinal_Equal : forall m m', Equal m m' -> cardinal m = cardinal m'.
-  Proof.
-  unfold cardinal; intros.
-  apply eqlistA_length with (eqA:=eqke).
-  apply elements_Equal_eqlistA; auto.
-  Qed.
-
-  End Cardinal.
-
   Section Min_Max_Elt.
 
   (** We emulate two [max_elt] and [min_elt] functions. *)
@@ -977,26 +1109,6 @@ Module Properties (M: S).
   End Min_Max_Elt.
 
   Section Induction_Principles.
- 
-  Lemma map_induction :
-   forall P : t elt -> Type,
-   (forall m, Empty m -> P m) ->
-   (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') ->
-   forall m, P m.
-  Proof.
-  intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.
-  apply X; apply cardinal_inv_1; auto.
-
-  destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *.
-  assert (Add x e (remove x m) m).
-   red; intros.
-   rewrite add_o; rewrite remove_o; destruct (ME.eq_dec x y); eauto with map.
-  apply X0 with (remove x m) x e; auto with map.
-  apply IHn; auto with map.
-  assert (S n = S (cardinal (remove x m))).
-   rewrite Heqn; eapply cardinal_2; eauto with map.
-  inversion H1; auto with map.
-  Qed.
 
   Lemma map_induction_max :
    forall P : t elt -> Type,
@@ -1011,7 +1123,7 @@ Module Properties (M: S).
   destruct p.
   assert (Add k e (remove k m) m).
    red; intros.
-   rewrite add_o; rewrite remove_o; destruct (ME.eq_dec k y); eauto.
+   rewrite add_o; rewrite remove_o; destruct (eq_dec k y); eauto.
    apply find_1; apply MapsTo_1 with k; auto.
    apply max_elt_MapsTo; auto.
   apply X0 with (remove k m) k e; auto with map.
@@ -1038,7 +1150,7 @@ Module Properties (M: S).
   destruct p.
   assert (Add k e (remove k m) m).
    red; intros.
-   rewrite add_o; rewrite remove_o; destruct (ME.eq_dec k y); eauto.
+   rewrite add_o; rewrite remove_o; destruct (eq_dec k y); eauto.
    apply find_1; apply MapsTo_1 with k; auto.
    apply min_elt_MapsTo; auto.
   apply X0 with (remove k m) k e; auto.
@@ -1056,13 +1168,8 @@ Module Properties (M: S).
 
   Section Fold_properties.
 
-  Lemma fold_Empty : forall s (A:Set)(f:key->elt->A->A)(i:A),
-   Empty s -> fold f s i = i.
-  Proof.
-  intros.
-  rewrite fold_1.
-  rewrite elements_Empty in H; rewrite H; simpl; auto.
-  Qed.
+  (** The following lemma has already been proved on Weak Maps,
+      but with one additionnal hypothesis (some [transpose] fact). *)
 
   Lemma fold_Equal : forall s1 s2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
    (f:key->elt->A->A)(i:A), 
@@ -1138,5 +1245,7 @@ Module Properties (M: S).
 
  End Elt.
 
-End Properties.
+End OrdProperties.
+
+
 
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index c235976bd..53173e968 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -10,25 +10,45 @@
 
 (** * Finite map library *)  
 
-(** This file proposes an interface for finite maps *)
+(** This file proposes interfaces for finite maps *)
 
-Require Export Bool OrderedType.
+Require Export Bool DecidableType OrderedType.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** When compared with Ocaml Map, this signature has been split in two: 
-   - The first part [S] contains the usual operators (add, find, ...)
-     It only requires a ordered key type, the data type can be arbitrary. 
-     The only function that asks more is [equal], whose first argument should 
-     be an equality on data. 
-   - Then, [Sord] extends [S] with a complete comparison function. For 
-     that, the data type should have a decidable total ordering. 
+(** When compared with Ocaml Map, this signature has been split in 
+    several parts : 
+
+   - The first parts [WSfun] and [WS] propose signatures for weak
+     maps, which are maps with no ordering on the key type nor the
+     data type.  [WSfun] and [WS] are almost identical, apart from the
+     fact that [WSfun] is expressed in a functorial way whereas [WS]
+     is self-contained. For obtaining an instance of such signatures,
+     a decidable equality on keys in enough (see for instance
+     [FMapWeakList]). These signatures contain the usual operators
+     (add, find, ...). The only function that asks for more is
+     [equal], whose first argument should be a comparison on data.
+ 
+   - Then comes [Sfun] and [S], that extend [WSfun] and [WS] to the 
+     case where the key type is ordered. The main addition states that 
+     [elements] produces sorted lists.
+
+   - Finally, [Sord] extends [S] with a complete comparison function. For 
+     that, the data type should have a decidable total ordering as well. 
 *)
 
 
-Module Type S.
 
-  Declare Module E : OrderedType.
+(** ** Weak Signature for maps
+   
+    No requirements for an ordering on elements, only decidability 
+    of equality. First, a functorial signature: *)
+
+Module Type WSfun (E : EqualityType).
+
+  (** The module E of base objects is meant to be a DecidableType
+     (and used to be so). But requiring only an EqualityType here
+     allows subtyping between FMap and FMapWeak *)
 
   Definition key := E.t.
 
@@ -125,8 +145,6 @@ Module Type S.
       Definition eq_key_elt (p p':key*elt) := 
           E.eq (fst p) (fst p') /\ (snd p) = (snd p').
 
-      Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
-
     (** Specification of [MapsTo] *)
       Parameter MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m.
       
@@ -160,9 +178,8 @@ Module Type S.
         MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
       Parameter elements_2 : 
         InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
-      Parameter elements_3 : sort lt_key (elements m).  
-      (* We add artificially elements_3w, a weaker version of 
-         elements_3, for allowing FMapWeak < FMap subtyping. *)
+      (** When compared with ordered FMap, here comes the only 
+         property that is really weaker: *)
       Parameter elements_3w : NoDupA eq_key (elements m).  
 
     (** Specification of [fold] *)  
@@ -206,7 +223,7 @@ Module Type S.
 	(x:key)(f:option elt->option elt'->option elt''), 
         In x (map2 f m m') -> In x m \/ In x m'.
 
-  Hint Immediate MapsTo_1 mem_2 is_empty_2 
+  Hint Immediate MapsTo_1 mem_2 is_empty_2
     map_2 mapi_2 add_3 remove_3 find_2
     : map.
   Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
@@ -215,11 +232,40 @@ Module Type S.
   (** for compatibility with earlier hints *)
   Hint Resolve map_2 mapi_2 add_3 remove_3 find_2 : oldmap.
 
+End WSfun.
+
+(** ** Main signature [WS] for Weak Maps 
+
+    Similar to [WSfun] but expressed in a self-contained way. *)
+
+Module Type WS. 
+  Declare Module E : EqualityType.
+  Include Type WSfun E.
+End WS.
+
+(** ** Maps on ordered keys, functorial signature *)
+
+Module Type Sfun (E : OrderedType).
+  Include Type WSfun E.
+  Section elt.
+  Variable elt:Set.
+   Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
+   (* Additionnal specification of [elements] *)
+   Parameter elements_3 : forall m, sort lt_key (elements m).
+  End elt.
+End Sfun.
+
+(** ** Maps on ordered keys, self-contained signature *)
+
+Module Type S. 
+  Declare Module E : OrderedType.
+  Include Type Sfun E.
 End S.
 
+(** ** Maps with ordering both on keys and datas *)
 
 Module Type Sord.
- 
+
   Declare Module Data : OrderedType.   
   Declare Module MapS : S. 
   Import MapS.
@@ -245,4 +291,4 @@ Module Type Sord.
       is a total ordering used to compare data associated with equal keys 
       in the two maps. *)
 
-End Sord.
\ No newline at end of file
+End Sord.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index b2cedaabb..b86e558b3 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -14,7 +14,6 @@
  [FMapInterface.S] using lists of pairs ordered (increasing) with respect to
  left projection. *)
 
-Require Import FSetInterface. 
 Require Import FMapInterface.
 
 Set Implicit Arguments.
@@ -23,10 +22,8 @@ Unset Strict Implicit.
 Module Raw (X:OrderedType).
 
 Module E := X.
-Module MX := OrderedTypeFacts X.
-Module PX := KeyOrderedType X.
-Import MX. 
-Import PX. 
+Module Import MX := OrderedTypeFacts X.
+Module Import PX := KeyOrderedType X.
 
 Definition key := X.t.
 Definition t (elt:Set) := list (X.t * elt).
diff --git a/theories/FSets/FMapWeak.v b/theories/FSets/FMapWeak.v
deleted file mode 100644
index a04ace03c..000000000
--- a/theories/FSets/FMapWeak.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Require Export DecidableType.
-Require Export DecidableTypeEx.
-Require Export FMapWeakInterface.
-Require Export FMapWeakList.
-Require Export FMapWeakFacts.
\ No newline at end of file
diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
deleted file mode 100644
index fbf761d8e..000000000
--- a/theories/FSets/FMapWeakFacts.v
+++ /dev/null
@@ -1,763 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(** * Finite maps library *)
-
-(** This functor derives additional facts from [FMapWeakInterface.S]. These
-  facts are mainly the specifications of [FMapWeakInterface.S] written using 
-  different styles: equivalence and boolean equalities. 
-*)
-
-Require Import Bool.
-Require Import OrderedType.
-Require Export FMapWeakInterface. 
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-Module Facts (M:S)(D:DecidableType with Definition t:=M.E.t 
-                                   with Definition eq:=M.E.eq).
-Import M.
-
-Notation eq_dec := D.eq_dec.
-Definition eqb x y := if eq_dec x y then true else false.
-
-Lemma MapsTo_fun : forall (elt:Set) m x (e e':elt), 
-  MapsTo x e m -> MapsTo x e' m -> e=e'.
-Proof.
-intros.
-generalize (find_1 H) (find_1 H0); clear H H0.
-intros; rewrite H in H0; injection H0; auto.
-Qed.
-
-(** * Specifications written using equivalences *)
-
-Section IffSpec. 
-Variable elt elt' elt'': Set.
-Implicit Type m: t elt.
-Implicit Type x y z: key.
-Implicit Type e: elt.
-
-Lemma MapsTo_iff : forall m x y e, E.eq x y -> (MapsTo x e m <-> MapsTo y e m).
-Proof.
-split; apply MapsTo_1; auto.
-Qed.
-
-Lemma In_iff : forall m x y, E.eq x y -> (In x m <-> In y m).
-Proof.
-unfold In.
-split; intros (e0,H0); exists e0.
-apply (MapsTo_1 H H0); auto.
-apply (MapsTo_1 (E.eq_sym H) H0); auto.
-Qed.
-
-Lemma find_mapsto_iff : forall m x e, MapsTo x e m <-> find x m = Some e.
-Proof.
-split; [apply find_1|apply find_2].
-Qed.
-
-Lemma not_find_mapsto_iff : forall m x, ~In x m <-> find x m = None.
-Proof.
-intros.
-generalize (find_mapsto_iff m x); destruct (find x m).
-split; intros; try discriminate.
-destruct H0.
-exists e; rewrite H; auto.
-split; auto.
-intros; intros (e,H1).
-rewrite H in H1; discriminate.
-Qed.
-
-Lemma mem_in_iff : forall m x, In x m <-> mem x m = true.
-Proof.
-split; [apply mem_1|apply mem_2].
-Qed.
-
-Lemma not_mem_in_iff : forall m x, ~In x m <-> mem x m = false.
-Proof.
-intros; rewrite mem_in_iff; destruct (mem x m); intuition.
-Qed.
-
-Lemma equal_iff : forall m m' cmp, Equal cmp m m' <-> equal cmp m m' = true.
-Proof. 
-split; [apply equal_1|apply equal_2].
-Qed.
-
-Lemma empty_mapsto_iff : forall x e, MapsTo x e (empty elt) <-> False.
-Proof.
-intuition; apply (empty_1 H).
-Qed.
-
-Lemma empty_in_iff : forall x, In x (empty elt) <-> False.
-Proof.
-unfold In.
-split; [intros (e,H); rewrite empty_mapsto_iff in H|]; intuition.
-Qed.
-
-Lemma is_empty_iff : forall m, Empty m <-> is_empty m = true. 
-Proof. 
-split; [apply is_empty_1|apply is_empty_2].
-Qed.
-
-Lemma add_mapsto_iff : forall m x y e e', 
-  MapsTo y e' (add x e m) <-> 
-     (E.eq x y /\ e=e') \/ 
-     (~E.eq x y /\ MapsTo y e' m).
-Proof. 
-intros.
-intuition.
-destruct (eq_dec x y); [left|right].
-split; auto.
-symmetry; apply (MapsTo_fun (e':=e) H); auto with map.
-split; auto; apply add_3 with x e; auto.
-subst; auto with map.
-Qed.
-
-Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m.
-Proof. 
-unfold In; split.
-intros (e',H).
-destruct (eq_dec x y) as [E|E]; auto.
-right; exists e'; auto.
-apply (add_3 E H).
-destruct (eq_dec x y) as [E|E]; auto.
-intros.
-exists e; apply add_1; auto.
-intros [H|(e',H)].
-destruct E; auto.
-exists e'; apply add_2; auto.
-Qed.
-
-Lemma add_neq_mapsto_iff : forall m x y e e', 
- ~ E.eq x y -> (MapsTo y e' (add x e m)  <-> MapsTo y e' m).
-Proof.
-split; [apply add_3|apply add_2]; auto.
-Qed.
-
-Lemma add_neq_in_iff : forall m x y e, 
- ~ E.eq x y -> (In y (add x e m)  <-> In y m).
-Proof.
-split; intros (e',H0); exists e'.
-apply (add_3 H H0).
-apply add_2; auto.
-Qed.
-
-Lemma remove_mapsto_iff : forall m x y e, 
-  MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m.
-Proof. 
-intros.
-split; intros.
-split.
-assert (In y (remove x m)) by (exists e; auto).
-intro H1; apply (remove_1 H1 H0).
-apply remove_3 with x; auto.
-apply remove_2; intuition.
-Qed.
-
-Lemma remove_in_iff : forall m x y, In y (remove x m) <-> ~E.eq x y /\ In y m.
-Proof. 
-unfold In; split.
-intros (e,H).
-split.
-assert (In y (remove x m)) by (exists e; auto).
-intro H1; apply (remove_1 H1 H0).
-exists e; apply remove_3 with x; auto.
-intros (H,(e,H0)); exists e; apply remove_2; auto.
-Qed.
-
-Lemma remove_neq_mapsto_iff : forall m x y e, 
- ~ E.eq x y -> (MapsTo y e (remove x m)  <-> MapsTo y e m).
-Proof.
-split; [apply remove_3|apply remove_2]; auto.
-Qed.
-
-Lemma remove_neq_in_iff : forall m x y, 
- ~ E.eq x y -> (In y (remove x m)  <-> In y m).
-Proof.
-split; intros (e',H0); exists e'.
-apply (remove_3 H0).
-apply remove_2; auto.
-Qed.
-
-Lemma elements_mapsto_iff : forall m x e, 
- MapsTo x e m <-> InA (@eq_key_elt _) (x,e) (elements m).
-Proof. 
-split; [apply elements_1 | apply elements_2].
-Qed.
-
-Lemma elements_in_iff : forall m x, 
- In x m <-> exists e, InA (@eq_key_elt _) (x,e) (elements m).
-Proof. 
-unfold In; split; intros (e,H); exists e; [apply elements_1 | apply elements_2]; auto.
-Qed.
-
-Lemma map_mapsto_iff : forall m x b (f : elt -> elt'), 
- MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m.
-Proof.
-split.
-case_eq (find x m); intros.
-exists e.
-split.
-apply (MapsTo_fun (m:=map f m) (x:=x)); auto with map.
-apply find_2; auto with map.
-assert (In x (map f m)) by (exists b; auto).
-destruct (map_2 H1) as (a,H2).
-rewrite (find_1 H2) in H; discriminate.
-intros (a,(H,H0)).
-subst b; auto with map.
-Qed.
-
-Lemma map_in_iff : forall m x (f : elt -> elt'), 
- In x (map f m) <-> In x m.
-Proof.
-split; intros; eauto with map.
-destruct H as (a,H).
-exists (f a); auto with map.
-Qed.
-
-Lemma mapi_in_iff : forall m x (f:key->elt->elt'),
- In x (mapi f m) <-> In x m.
-Proof.
-split; intros; eauto with map.
-destruct H as (a,H).
-destruct (mapi_1 f H) as (y,(H0,H1)).
-exists (f y a); auto.
-Qed.
-
-(* Unfortunately, we don't have simple equivalences for [mapi] 
-  and [MapsTo]. The only correct one needs compatibility of [f]. *) 
-
-Lemma mapi_inv : forall m x b (f : key -> elt -> elt'), 
- MapsTo x b (mapi f m) -> 
- exists a, exists y, E.eq y x /\ b = f y a /\ MapsTo x a m.
-Proof.
-intros; case_eq (find x m); intros.
-exists e.
-destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)).
-apply find_2; auto with map.
-exists y; repeat split; auto with map.
-apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto with map.
-assert (In x (mapi f m)) by (exists b; auto).
-destruct (mapi_2 H1) as (a,H2).
-rewrite (find_1 H2) in H0; discriminate.
-Qed.
-
-Lemma mapi_1bis : forall m x e (f:key->elt->elt'), 
- (forall x y e, E.eq x y -> f x e = f y e) -> 
- MapsTo x e m -> MapsTo x (f x e) (mapi f m).
-Proof.
-intros.
-destruct (mapi_1 f H0) as (y,(H1,H2)).
-replace (f x e) with (f y e) by auto.
-auto.
-Qed.
-
-Lemma mapi_mapsto_iff : forall m x b (f:key->elt->elt'),
- (forall x y e, E.eq x y -> f x e = f y e) -> 
- (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m).
-Proof.
-split.
-intros.
-destruct (mapi_inv H0) as (a,(y,(H1,(H2,H3)))).
-exists a; split; auto.
-subst b; auto.
-intros (a,(H0,H1)).
-subst b.
-apply mapi_1bis; auto.
-Qed.
-
-(** Things are even worse for [map2] : we don't try to state any 
- equivalence, see instead boolean results below. *)
-
-End IffSpec.
-
-(** Useful tactic for simplifying expressions like [In y (add x e (remove z m))] *)
-  
-Ltac map_iff := 
- repeat (progress (
-  rewrite add_mapsto_iff || rewrite add_in_iff ||
-  rewrite remove_mapsto_iff || rewrite remove_in_iff ||
-  rewrite empty_mapsto_iff || rewrite empty_in_iff ||
-  rewrite map_mapsto_iff || rewrite map_in_iff ||
-  rewrite mapi_in_iff)).
-
-(**  * Specifications written using boolean predicates *)
-
-Section BoolSpec.
-
-Lemma mem_find_b : forall (elt:Set)(m:t elt)(x:key), mem x m = if find x m then true else false. 
-Proof.
-intros.
-generalize (find_mapsto_iff m x)(mem_in_iff m x); unfold In.
-destruct (find x m); destruct (mem x m); auto.
-intros.
-rewrite <- H0; exists e; rewrite H; auto.
-intuition.
-destruct H0 as (e,H0).
-destruct (H e); intuition discriminate.
-Qed.
-
-Variable elt elt' elt'' : Set.
-Implicit Types m : t elt.
-Implicit Types x y z : key.
-Implicit Types e : elt.
-
-Lemma mem_b : forall m x y, E.eq x y -> mem x m = mem y m.
-Proof. 
-intros.
-generalize (mem_in_iff m x) (mem_in_iff m y)(In_iff m H).
-destruct (mem x m); destruct (mem y m); intuition.
-Qed.
-
-Lemma find_o : forall m x y, E.eq x y -> find x m = find y m.
-Proof.
-intros.
-generalize (find_mapsto_iff m x) (find_mapsto_iff m y) (fun e => MapsTo_iff m e H).
-destruct (find x m); destruct (find y m); intros.
-rewrite <- H0; rewrite H2; rewrite H1; auto.
-symmetry; rewrite <- H1; rewrite <- H2; rewrite H0; auto.
-rewrite <- H0; rewrite H2; rewrite H1; auto.
-auto.
-Qed.
-
-Lemma empty_o : forall x, find x (empty elt) = None.
-Proof.
-intros.
-case_eq (find x (empty elt)); intros; auto.
-generalize (find_2 H).
-rewrite empty_mapsto_iff; intuition.
-Qed.
-
-Lemma empty_a : forall x, mem x (empty elt) = false.
-Proof.
-intros.
-case_eq (mem x (empty elt)); intros; auto.
-generalize (mem_2 H).
-rewrite empty_in_iff; intuition.
-Qed.
-
-Lemma add_eq_o : forall m x y e, 
- E.eq x y -> find y (add x e m) = Some e.
-Proof.
-auto with map.
-Qed.
-
-Lemma add_neq_o : forall m x y e, 
- ~ E.eq x y -> find y (add x e m) = find y m. 
-Proof.
-intros.
-case_eq (find y m); intros; auto with map.
-case_eq (find y (add x e m)); intros; auto with map.
-rewrite <- H0; symmetry.
-apply find_1; apply add_3 with x e; auto with map.
-Qed.
-Hint Resolve add_neq_o : map.
-
-Lemma add_o : forall m x y e, 
- find y (add x e m) = if eq_dec x y then Some e else find y m.
-Proof.
-intros; destruct (eq_dec x y); auto with map.
-Qed.
-
-Lemma add_eq_b : forall m x y e, 
- E.eq x y -> mem y (add x e m) = true.
-Proof.
-intros; rewrite mem_find_b; rewrite add_eq_o; auto.
-Qed.
-
-Lemma add_neq_b : forall m x y e, 
- ~E.eq x y -> mem y (add x e m) = mem y m.
-Proof.
-intros; do 2 rewrite mem_find_b; rewrite add_neq_o; auto.
-Qed.
-
-Lemma add_b : forall m x y e, 
- mem y (add x e m) = eqb x y || mem y m. 
-Proof.
-intros; do 2 rewrite mem_find_b; rewrite add_o; unfold eqb.
-destruct (eq_dec x y); simpl; auto.
-Qed.
-
-Lemma remove_eq_o : forall m x y, 
- E.eq x y -> find y (remove x m) = None.
-Proof.
-intros.
-generalize (remove_1 (m:=m) H).
-generalize (find_mapsto_iff (remove x m) y).
-destruct (find y (remove x m)); auto.
-destruct 2.
-exists e; rewrite H0; auto.
-Qed.
-Hint Resolve remove_eq_o : map.
-
-Lemma remove_neq_o : forall m x y, 
- ~ E.eq x y -> find y (remove x m) = find y m. 
-Proof.
-intros.
-case_eq (find y m); intros; auto with map.
-case_eq (find y (remove x m)); intros; auto with map.
-rewrite <- H0; symmetry.
-apply find_1; apply remove_3 with x; auto with map.
-Qed.
-Hint Resolve remove_neq_o : map.
-
-Lemma remove_o : forall m x y, 
- find y (remove x m) = if eq_dec x y then None else find y m.
-Proof.
-intros; destruct (eq_dec x y); auto with map.
-Qed.
-
-Lemma remove_eq_b : forall m x y, 
- E.eq x y -> mem y (remove x m) = false.
-Proof.
-intros; rewrite mem_find_b; rewrite remove_eq_o; auto.
-Qed.
-
-Lemma remove_neq_b : forall m x y, 
- ~ E.eq x y -> mem y (remove x m) = mem y m.
-Proof.
-intros; do 2 rewrite mem_find_b; rewrite remove_neq_o; auto.
-Qed.
-
-Lemma remove_b : forall m x y, 
- mem y (remove x m) = negb (eqb x y) && mem y m.
-Proof.
-intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb.
-destruct (eq_dec x y); auto.
-Qed.
-
-Definition option_map (A:Set)(B:Set)(f:A->B)(o:option A) : option B := 
- match o with 
-  | Some a => Some (f a)
-  | None => None
- end.
-
-Lemma map_o : forall m x (f:elt->elt'), 
- find x (map f m) = option_map f (find x m). 
-Proof.
-intros.
-generalize (find_mapsto_iff (map f m) x) (find_mapsto_iff m x)
-  (fun b => map_mapsto_iff m x b f).
-destruct (find x (map f m)); destruct (find x m); simpl; auto; intros.
-rewrite <- H; rewrite H1; exists e0; rewrite H0; auto.
-destruct (H e) as [_ H2].
-rewrite H1 in H2.
-destruct H2 as (a,(_,H2)); auto.
-rewrite H0 in H2; discriminate.
-rewrite <- H; rewrite H1; exists e; rewrite H0; auto.
-Qed.
-
-Lemma map_b : forall m x (f:elt->elt'), 
- mem x (map f m) = mem x m.
-Proof.
-intros; do 2 rewrite mem_find_b; rewrite map_o.
-destruct (find x m); simpl; auto.
-Qed.
-
-Lemma mapi_b : forall m x (f:key->elt->elt'), 
- mem x (mapi f m) = mem x m.
-Proof.
-intros.
-generalize (mem_in_iff (mapi f m) x) (mem_in_iff m x) (mapi_in_iff m x f).
-destruct (mem x (mapi f m)); destruct (mem x m); simpl; auto; intros.
-symmetry; rewrite <- H0; rewrite <- H1; rewrite H; auto.
-rewrite <- H; rewrite H1; rewrite H0; auto.
-Qed.
-
-Lemma mapi_o : forall m x (f:key->elt->elt'), 
- (forall x y e, E.eq x y -> f x e = f y e) -> 
- find x (mapi f m) = option_map (f x) (find x m).
-Proof.
-intros.
-generalize (find_mapsto_iff (mapi f m) x) (find_mapsto_iff m x) 
-  (fun b => mapi_mapsto_iff m x b H).
-destruct (find x (mapi f m)); destruct (find x m); simpl; auto; intros.
-rewrite <- H0; rewrite H2; exists e0; rewrite H1; auto.
-destruct (H0 e) as [_ H3].
-rewrite H2 in H3.
-destruct H3 as (a,(_,H3)); auto.
-rewrite H1 in H3; discriminate.
-rewrite <- H0; rewrite H2; exists e; rewrite H1; auto.
-Qed.
-
-Lemma map2_1bis : forall (m: t elt)(m': t elt') x 
- (f:option elt->option elt'->option elt''), 
- f None None = None -> 
- find x (map2 f m m') = f (find x m) (find x m').       
-Proof.
-intros.
-case_eq (find x m); intros.
-rewrite <- H0.
-apply map2_1; auto with map.
-left; exists e; auto with map.
-case_eq (find x m'); intros.
-rewrite <- H0; rewrite <- H1.
-apply map2_1; auto.
-right; exists e; auto with map.
-rewrite H.
-case_eq (find x (map2 f m m')); intros; auto with map.
-assert (In x (map2 f m m')) by (exists e; auto with map).
-destruct (map2_2 H3) as [(e0,H4)|(e0,H4)].
-rewrite (find_1 H4) in H0; discriminate.
-rewrite (find_1 H4) in H1; discriminate.
-Qed.
-
-Lemma elements_o : forall m x, 
- find x m = findA (eqb x) (elements m).
-Proof.
-intros.
-assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)).
- intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff.
-assert (NoDupA (eq_key (elt:=elt)) (elements m)). 
- exact (elements_3w m).
-generalize (fun e => @findA_NoDupA _ _ _ D.eq_sym D.eq_trans eq_dec (elements m) x e H0).
-unfold eqb.
-destruct (find x m); destruct (findA (fun y:D.t => if eq_dec x y then true else false) (elements m)); 
- simpl; auto; intros.
-symmetry; rewrite <- H1; rewrite <- H; auto.
-symmetry; rewrite <- H1; rewrite <- H; auto.
-rewrite H; rewrite H1; auto.
-Qed.
-
-Lemma elements_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (elements m).
-Proof.
-intros.
-generalize (mem_in_iff m x)(elements_in_iff m x)
- (existsb_exists (fun p => eqb x (fst p)) (elements m)).
-destruct (mem x m); destruct (existsb (fun p => eqb x (fst p)) (elements m)); auto; intros.
-symmetry; rewrite H1.
-destruct H0 as (H0,_).
-destruct H0 as (e,He); [ intuition |].
-rewrite InA_alt in He.
-destruct He as ((y,e'),(Ha1,Ha2)).
-compute in Ha1; destruct Ha1; subst e'.
-exists (y,e); split; simpl; auto.
-unfold eqb; destruct (eq_dec x y); intuition.
-rewrite <- H; rewrite H0.
-destruct H1 as (H1,_).
-destruct H1 as ((y,e),(Ha1,Ha2)); [intuition|].
-simpl in Ha2.
-unfold eqb in *; destruct (eq_dec x y); auto; try discriminate.
-exists e; rewrite InA_alt.
-exists (y,e); intuition.
-compute; auto.
-Qed.
-
-End BoolSpec.
-
-End Facts.
-
-
-Module Properties 
- (M:S)(D:DecidableType with Definition t:=M.E.t 
-                       with Definition eq:=M.E.eq).
- Module F:=Facts M D. 
- Import F.
- Import M.
-
- Section Elt. 
-  Variable elt:Set.
-
-  Definition cardinal (m:t elt) := length (elements m).
-
-  Definition Equal (m m':t elt) := forall y, find y m = find y m'.
-  Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).
-
-  Notation eqke := (@eq_key_elt elt).
-  Notation eqk := (@eq_key elt).
-
-  Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil.
-  Proof.
-  intros.
-  unfold Empty.
-  split; intros.
-  assert (forall a, ~ List.In a (elements m)).
-   red; intros.
-   apply (H (fst a) (snd a)).
-   rewrite elements_mapsto_iff.
-   rewrite InA_alt; exists a; auto.
-   split; auto; split; auto.
-  destruct (elements m); auto.
-  elim (H0 p); simpl; auto.
-  red; intros.
-  rewrite elements_mapsto_iff in H0.
-  rewrite InA_alt in H0; destruct H0.
-  rewrite H in H0; destruct H0 as (_,H0); inversion H0.
-  Qed.
-
-  Lemma fold_Empty : forall m (A:Set)(f:key->elt->A->A)(i:A),
-   Empty m -> fold f m i = i.
-  Proof.
-  intros.
-  rewrite fold_1.
-  rewrite elements_Empty in H; rewrite H; simpl; auto.
-  Qed.
-
-  Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l.
-  Proof.
-  induction 1; auto.
-  constructor; auto.
-  contradict H.
-  destruct x as (x,y).
-  rewrite InA_alt in *; destruct H as ((a,b),((H1,H2),H3)); simpl in *.
-  exists (a,b); auto.
-  Qed.
-
-  Lemma fold_Equal : forall m1 m2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
-   (f:key->elt->A->A)(i:A), 
-   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
-   transpose eqA (fun y => f (fst y) (snd y)) -> 
-   Equal m1 m2 -> 
-   eqA (fold f m1 i) (fold f m2 i).
-  Proof.
-  assert (eqke_refl : forall p, eqke p p).
-   red; auto.
-  assert (eqke_sym : forall p p', eqke p p' -> eqke p' p).
-   intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition.
-  assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p'').
-   intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
-   intuition; eauto; congruence.
-  intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
-  apply fold_right_equivlistA with (eqA:=eqke) (eqB:=eqA); auto.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  red; intros.
-  do 2 rewrite InA_rev.
-  destruct x; do 2 rewrite <- elements_mapsto_iff.
-  do 2 rewrite find_mapsto_iff.
-  rewrite H1; split; auto.
-  Qed.
-
-  Lemma fold_Add : forall m1 m2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
-   (f:key->elt->A->A)(i:A), 
-   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
-   transpose eqA (fun y =>f (fst y) (snd y)) -> 
-   ~In x m1 -> Add x e m1 m2 -> 
-   eqA (fold f m2 i) (f x e (fold f m1 i)).
-  Proof.
-  assert (eqke_refl : forall p, eqke p p).
-   red; auto.
-  assert (eqke_sym : forall p p', eqke p p' -> eqke p' p).
-   intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition.
-  assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p'').
-   intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
-   intuition; eauto; congruence.
-  intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
-  set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
-  change (f x e (fold_right f' i (rev (elements m1))))
-   with (f' (x,e) (fold_right f' i (rev (elements m1)))).
-  apply fold_right_add with (eqA:=eqke)(eqB:=eqA); auto.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  rewrite InA_rev.
-  contradict H1.
-  exists e.
-  rewrite elements_mapsto_iff; auto.
-  intros a.
-  rewrite InA_cons; do 2 rewrite InA_rev; 
-  destruct a as (a,b); do 2 rewrite <- elements_mapsto_iff.
-  do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl.
-  rewrite H2.
-  rewrite add_o.
-  destruct (eq_dec x a); intuition.
-  inversion H3; auto.
-  f_equal; auto.
-  elim H1.
-  exists b; apply MapsTo_1 with a; auto with map.
-  elim n; auto.
-  Qed.
-
-  Lemma cardinal_fold : forall m, cardinal m = fold (fun _ _ => S) m 0.
-  Proof.
-  intros; unfold cardinal; rewrite fold_1.
-  symmetry; apply fold_left_length; auto.
-  Qed.
- 
-  Lemma Equal_cardinal : forall m m', Equal m m' -> cardinal m = cardinal m'.
-  Proof.
-  intros; do 2 rewrite cardinal_fold.
-  apply fold_Equal with (eqA:=@eq _); auto.
-  constructor; auto; congruence.
-  red; auto.
-  red; auto.
-  Qed.
-
-  Lemma cardinal_1 : forall m, Empty m -> cardinal m = 0.
-  Proof.
-  intros; unfold cardinal; rewrite elements_Empty in H; rewrite H; simpl; auto.
-  Qed.
-
-  Lemma cardinal_2 :
-    forall m m' x e, ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m).
-  Proof.
-  intros; do 2 rewrite cardinal_fold.
-  change S with ((fun _ _ => S) x e).
-  apply fold_Add; auto.
-  constructor; intros; auto; congruence.
-  red; simpl; auto.
-  red; simpl; auto.
-  Qed.
-
-  Lemma cardinal_inv_1 : forall m, cardinal m = 0 -> Empty m. 
-  Proof. 
-  unfold cardinal; intros m H a e.
-  rewrite elements_mapsto_iff.    
-  destruct (elements m); simpl in *.
-  red; inversion 1.
-  inversion H.
-  Qed.
-  Hint Resolve cardinal_inv_1 : map.
-
-  Lemma cardinal_inv_2 :
-   forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
-  Proof. 
-  unfold cardinal; intros.
-  generalize (elements_mapsto_iff m).
-  destruct (elements m); try discriminate. 
-  exists p; auto.
-  rewrite H0; destruct p; simpl; auto.
-  constructor; red; auto.
-  Qed.
-
-  Lemma cardinal_inv_2b :
-   forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }.
-  Proof. 
-    intros; unfold cardinal in *.
-    generalize (elements_2 (m:=m)).
-    destruct (elements m).
-    simpl in H; elim H; auto.
-    exists p; auto.
-    destruct p; simpl; auto.
-    apply H0; constructor; red; auto.
-  Qed.
-
-  Lemma map_induction :
-   forall P : t elt -> Type,
-   (forall m, Empty m -> P m) ->
-   (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') ->
-   forall m, P m.
-  Proof.
-  intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.
-  apply X; apply cardinal_inv_1; auto.
-
-  destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *.
-  assert (Add x e (remove x m) m).
-   red; intros.
-   rewrite add_o; rewrite remove_o; destruct (eq_dec x y); eauto with map.
-  apply X0 with (remove x m) x e; auto with map.
-  apply IHn; auto with map.
-  assert (S n = S (cardinal (remove x m))).
-   rewrite Heqn; eapply cardinal_2; eauto with map.
-  inversion H1; auto with map.
-  Qed.
-
- End Elt.
-
-End Properties.
-
diff --git a/theories/FSets/FMapWeakInterface.v b/theories/FSets/FMapWeakInterface.v
deleted file mode 100644
index 49dcb5214..000000000
--- a/theories/FSets/FMapWeakInterface.v
+++ /dev/null
@@ -1,209 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(** * Finite map library *) 
-
-(** This file proposes an interface for finite maps over keys with decidable 
-     equality, but no decidable order. *)
-
-Require Export Bool DecidableType.
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-Module Type S.
-
-  (** The module E of base objects is meant to be a DecidableType
-     (and used to be so). But requiring only an EqualityType here
-     allows subtyping between FMap and FMapWeak *)
-  Declare Module E : EqualityType.
-
-  Definition key := E.t.
-
-  Parameter t : Set -> Set. (** the abstract type of maps *)
- 
-  Section Types. 
-
-    Variable elt:Set.
-
-    Parameter empty : t elt.
-      (** The empty map. *)
-
-    Parameter is_empty : t elt -> bool.
-    (** Test whether a map is empty or not. *)
-
-    Parameter add : key -> elt -> t elt -> t elt.
-    (** [add x y m] returns a map containing the same bindings as [m], 
-	plus a binding of [x] to [y]. If [x] was already bound in [m], 
-	its previous binding disappears. *)
-
-    Parameter find : key -> t elt -> option elt. 
-    (** [find x m] returns the current binding of [x] in [m], 
-	or raises [Not_found] if no such binding exists.
-	NB: in Coq, the exception mechanism becomes a option type. *)
-
-    Parameter remove : key -> t elt -> t elt.
-    (** [remove x m] returns a map containing the same bindings as [m], 
-	except for [x] which is unbound in the returned map. *)
-
-    Parameter mem : key -> t elt -> bool.
-    (** [mem x m] returns [true] if [m] contains a binding for [x], 
-	and [false] otherwise. *)
-
-    (** Coq comment: [iter] is useless in a purely functional world *)
-    (** val iter : (key -> 'a -> unit) -> 'a t -> unit *)
-    (** iter f m applies f to all bindings in map m. f receives the key as 
-	first argument, and the associated value as second argument. 
-	The bindings are passed to f in increasing order with respect to the 
-	ordering over the type of the keys. Only current bindings are 
-	presented to f: bindings hidden by more recent bindings are not 
-	passed to f. *)
-
-    Variable elt' : Set. 
-    Variable elt'': Set.
-
-    Parameter map : (elt -> elt') -> t elt -> t elt'.
-    (** [map f m] returns a map with same domain as [m], where the associated 
-	value a of all bindings of [m] has been replaced by the result of the
-	application of [f] to [a]. The bindings are passed to [f] in 
-	increasing order with respect to the ordering over the type of the 
-	keys. *)
-
-    Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'.
-    (** Same as [S.map], but the function receives as arguments both the 
-	key and the associated value for each binding of the map. *)
-
-    Parameter map2 : (option elt -> option elt' -> option elt'') -> t elt -> t elt' ->  t elt''.
-    (** Not present in Ocaml. 
-         [map f m m'] creates a new map whose bindings belong to the ones of either 
-         [m] or [m']. The presence and value for a key [k] is determined by [f e e'] 
-         where [e] and [e'] are the (optional) bindings of [k] in [m] and [m']. *)
-
-    Parameter elements : t elt -> list (key*elt).
-    (** Not present in Ocaml. 
-         [elements m] returns an assoc list corresponding to the bindings of [m].
-         Elements of this list are sorted with respect to their first components. 
-         Useful to specify [fold] ... *)
-
-    Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A.
-    (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], 
-	where [k1] ... [kN] are the keys of all bindings in [m] 
-	(in increasing order), and [d1] ... [dN] are the associated data. *)
-
-    Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool.
-    (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are equal, 
-      that is, contain equal keys and associate them with equal data. 
-      [cmp] is the equality predicate used to compare the data associated 
-      with the keys. *)
-
-    Section Spec. 
-      
-      Variable m m' m'' : t elt.
-      Variable x y z : key.
-      Variable e e' : elt.
-
-      Parameter MapsTo : key -> elt -> t elt -> Prop.
-
-      Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m.
-
-      Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m.
-
-      Definition eq_key (p p':key*elt) := E.eq (fst p) (fst p').
-      
-      Definition eq_key_elt (p p':key*elt) := 
-          E.eq (fst p) (fst p') /\ (snd p) = (snd p').
-
-    (** Specification of [MapsTo] *)
-      Parameter MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m.
-      
-    (** Specification of [mem] *)
-      Parameter mem_1 : In x m -> mem x m = true.
-      Parameter mem_2 : mem x m = true -> In x m. 
-      
-    (** Specification of [empty] *)
-      Parameter empty_1 : Empty empty.
-
-    (** Specification of [is_empty] *)
-      Parameter is_empty_1 : Empty m -> is_empty m = true. 
-      Parameter is_empty_2 : is_empty m = true -> Empty m.
-      
-    (** Specification of [add] *)
-      Parameter add_1 : E.eq x y -> MapsTo y e (add x e m).
-      Parameter add_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
-      Parameter add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
-
-    (** Specification of [remove] *)
-      Parameter remove_1 : E.eq x y -> ~ In y (remove x m).
-      Parameter remove_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
-      Parameter remove_3 : MapsTo y e (remove x m) -> MapsTo y e m.
-
-    (** Specification of [find] *)
-      Parameter find_1 : MapsTo x e m -> find x m = Some e. 
-      Parameter find_2 : find x m = Some e -> MapsTo x e m.
-
-    (** Specification of [elements] *)
-      Parameter elements_1 : 
-        MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
-      Parameter elements_2 : 
-        InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
-      (** When compared with ordered FMap, here comes the only 
-         property that is really weaker: *)
-      Parameter elements_3w : NoDupA eq_key (elements m).  
-
-    (** Specification of [fold] *)  
-      Parameter fold_1 :
-	forall (A : Type) (i : A) (f : key -> elt -> A -> A),
-        fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
- 
-   Definition Equal cmp m m' := 
-         (forall k, In k m <-> In k m') /\ 
-         (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
-
-   Variable cmp : elt -> elt -> bool. 
-
-   (** Specification of [equal] *)
-     Parameter equal_1 : Equal cmp m m' -> equal cmp m m' = true. 
-     Parameter equal_2 : equal cmp m m' = true -> Equal cmp m m'.
-
-    End Spec. 
-   End Types. 
-
-    (** Specification of [map] *)
-      Parameter map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), 
-        MapsTo x e m -> MapsTo x (f e) (map f m).
-      Parameter map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), 
-        In x (map f m) -> In x m.
- 
-    (** Specification of [mapi] *)
-      Parameter mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)
-        (f:key->elt->elt'), MapsTo x e m -> 
-        exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
-      Parameter mapi_2 : forall (elt elt':Set)(m: t elt)(x:key)
-        (f:key->elt->elt'), In x (mapi f m) -> In x m.
-
-    (** Specification of [map2] *)
-      Parameter map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
-	(x:key)(f:option elt->option elt'->option elt''), 
-	In x m \/ In x m' -> 
-        find x (map2 f m m') = f (find x m) (find x m').       
-
-     Parameter map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
-	(x:key)(f:option elt->option elt'->option elt''), 
-        In x (map2 f m m') -> In x m \/ In x m'.
-
-  Hint Immediate MapsTo_1 mem_2 is_empty_2
-    map_2 mapi_2 add_3 remove_3 find_2
-    : map.
-  Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
-    remove_2 find_1 fold_1 map_1 mapi_1 mapi_2
-    : map.
-  (** for compatibility with earlier hints *)
-  Hint Resolve map_2 mapi_2 add_3 remove_3 find_2 : oldmap.
-
-End S.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index dca6e5498..579fd50c9 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -11,21 +11,16 @@
 (** * Finite map library *)  
 
 (** This file proposes an implementation of the non-dependant interface
- [FMapInterface.S] using lists of pairs,  unordered but without redundancy. *)
+ [FMapInterface.WS] using lists of pairs,  unordered but without redundancy. *)
 
-Require Import FSetInterface. 
-Require Import FSetWeakInterface.
-Require Import FMapWeakInterface.
+Require Import FMapInterface.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Arguments Scope list [type_scope].
-
 Module Raw (X:DecidableType).
 
-Module PX := KeyDecidableType X.
-Import PX.
+Module Import PX := KeyDecidableType X.
 
 Definition key := X.t.
 Definition t (elt:Set) := list (X.t * elt).
@@ -873,7 +868,7 @@ End Elt3.
 End Raw.
 
 
-Module Make (X: DecidableType) <: S with Module E:=X.
+Module Make (X: DecidableType) <: WS with Module E:=X.
  Module Raw := Raw X. 
 
  Module E := X.
diff --git a/theories/FSets/FMaps.v b/theories/FSets/FMaps.v
index f812e56e8..644f73a9e 100644
--- a/theories/FSets/FMaps.v
+++ b/theories/FSets/FMaps.v
@@ -8,9 +8,9 @@
 
 (* $Id$ *)
 
-Require Export OrderedType.
-Require Export OrderedTypeEx.
-Require Export OrderedTypeAlt.
+
+Require Export OrderedType OrderedTypeEx OrderedTypeAlt.
+Require Export DecidableType DecidableTypeEx.
 Require Export FMapInterface.
 Require Export FMapList.
 Require Export FMapPositive.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 825bdefed..d6a92b673 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -17,11 +17,11 @@
 (** This file implements a decision procedure for a certain
     class of propositions involving finite sets.  *)
 
-Require Import Decidable DecidableTypeEx FSetWeakFacts.
+Require Import Decidable DecidableTypeEx FSetFacts.
 
-Module WeakDecide 
- (Import M : FSetWeakInterface.S)
- (D:DecidableType with Definition t:=M.E.t with Definition eq:=M.E.eq).
+(** First, a version for Weak Sets *)
+
+Module WDecide (E : DecidableType)(Import M : WSfun E).
 
 (** * Overview
     This functor defines the tactic [fsetdec], which will
@@ -566,7 +566,7 @@ the above form:
         the predicates [In] and [E.eq] applied only to
         variables.  We are going to use them with [autorewrite].
         *)
-    Module F := FSetWeakFacts.Facts M D.
+    Module F := FSetFacts.WFacts E M.
     Hint Rewrite
       F.empty_iff F.singleton_iff F.add_iff F.remove_iff
       F.union_iff F.inter_iff F.diff_iff
@@ -585,7 +585,7 @@ the above form:
     Lemma dec_eq : forall (x y : E.t),
       decidable (E.eq x y).
     Proof.
-      red; intros x y; destruct (D.eq_dec x y); auto.
+      red; intros x y; destruct (E.eq_dec x y); auto.
     Qed.
 
     (** The hint database [FSet_decidability] will be given to
@@ -930,12 +930,15 @@ the above form:
 
   End FSetDecideTestCases.
 
-End WeakDecide.
+End WDecide.
 
 Require Import FSetInterface.
 
-Module Decide (M : FSetInterface.S).
+(** Now comes a special version dedicated to full sets. For this 
+    one, only one argument [(M:S)] is necessary. *)
+
+Module Decide (M : S).
   Module D:=OT_as_DT M.E.
-  Module WD := WeakDecide M D.
+  Module WD := WDecide D M.
   Ltac fsetdec := WD.fsetdec.
 End Decide.
\ No newline at end of file
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 89fae94e6..e0e83c57c 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -12,20 +12,928 @@
 
 (** This module proves many properties of finite sets that 
     are consequences of the axiomatization in [FsetInterface] 
-    Contrary to the functor in [FsetWeakProperties] it uses 
+    Contrary to the functor in [FsetProperties] it uses 
     sets operations instead of predicates over sets, i.e.
     [mem x s=true] instead of [In x s], 
     [equal s s'=true] instead of [Equal s s'], etc. *)
 
 Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.
 
-(** Since the properties that used to be there do not depend on 
-    the element ordering, we now simply import them from 
-    FSetWeakEqProperties *)
+Module WEqProperties (Import E:DecidableType)(M:WSfun E). 
+Module Import MP := WProperties E M.
+Import FM.
+Import M.
 
-Require FSetWeakEqProperties.
+Definition Add := MP.Add.
+
+Section BasicProperties. 
+
+(** Some old specifications written with boolean equalities. *) 
+
+Variable s s' s'': t.
+Variable x y z : elt.
+
+Lemma mem_eq: 
+  E.eq x y -> mem x s=mem y s.
+Proof. 
+intro H; rewrite H; auto.
+Qed.
+
+Lemma equal_mem_1: 
+  (forall a, mem a s=mem a s') -> equal s s'=true.
+Proof. 
+intros; apply equal_1; unfold Equal; intros.
+do 2 rewrite mem_iff; rewrite H; tauto.
+Qed.
+
+Lemma equal_mem_2: 
+  equal s s'=true -> forall a, mem a s=mem a s'.
+Proof. 
+intros; rewrite (equal_2 H); auto.
+Qed.
+
+Lemma subset_mem_1: 
+  (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
+Proof. 
+intros; apply subset_1; unfold Subset; intros a.
+do 2 rewrite mem_iff; auto.
+Qed.
+
+Lemma subset_mem_2: 
+  subset s s'=true -> forall a, mem a s=true -> mem a s'=true.
+Proof. 
+intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
+Qed.
+  
+Lemma empty_mem: mem x empty=false.
+Proof. 
+rewrite <- not_mem_iff; auto with set.
+Qed.
+
+Lemma is_empty_equal_empty: is_empty s = equal s empty.
+Proof. 
+apply bool_1; split; intros.
+rewrite <- (empty_is_empty_1 (s:=empty)); auto with set.
+rewrite <- is_empty_iff; auto with set.
+Qed.
+  
+Lemma choose_mem_1: choose s=Some x -> mem x s=true.
+Proof.  
+auto with set.
+Qed.
+
+Lemma choose_mem_2: choose s=None -> is_empty s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_mem_1: mem x (add x s)=true.
+Proof.
+auto with set.
+Qed.  
+ 
+Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
+Proof. 
+apply add_neq_b.
+Qed.
+
+Lemma remove_mem_1: mem x (remove x s)=false.
+Proof. 
+rewrite <- not_mem_iff; auto with set.
+Qed. 
+ 
+Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
+Proof. 
+apply remove_neq_b.
+Qed.
+
+Lemma singleton_equal_add: 
+  equal (singleton x) (add x empty)=true.
+Proof.
+rewrite (singleton_equal_add x); auto with set.
+Qed.  
+
+Lemma union_mem: 
+  mem x (union s s')=mem x s || mem x s'.
+Proof. 
+apply union_b.
+Qed.
+
+Lemma inter_mem: 
+  mem x (inter s s')=mem x s && mem x s'.
+Proof. 
+apply inter_b.
+Qed.
+
+Lemma diff_mem: 
+  mem x (diff s s')=mem x s && negb (mem x s').
+Proof. 
+apply diff_b.
+Qed.
+
+(** properties of [mem] *)
+
+Lemma mem_3 : ~In x s -> mem x s=false.
+Proof.
+intros; rewrite <- not_mem_iff; auto.
+Qed.
+
+Lemma mem_4 : mem x s=false -> ~In x s.
+Proof.
+intros; rewrite not_mem_iff; auto.
+Qed.
+
+(** Properties of [equal] *) 
+
+Lemma equal_refl: equal s s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma equal_sym: equal s s'=equal s' s.
+Proof.
+intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
+Qed.
+
+Lemma equal_trans: 
+ equal s s'=true -> equal s' s''=true -> equal s s''=true.
+Proof.
+intros; rewrite (equal_2 H); auto.
+Qed.
+
+Lemma equal_equal: 
+ equal s s'=true -> equal s s''=equal s' s''.
+Proof.
+intros; rewrite (equal_2 H); auto.
+Qed.
+
+Lemma equal_cardinal: 
+ equal s s'=true -> cardinal s=cardinal s'.
+Proof.
+auto with set.
+Qed.
+
+(* Properties of [subset] *)
+
+Lemma subset_refl: subset s s=true. 
+Proof.
+auto with set.
+Qed.
+
+Lemma subset_antisym: 
+ subset s s'=true -> subset s' s=true -> equal s s'=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma subset_trans: 
+ subset s s'=true -> subset s' s''=true -> subset s s''=true.
+Proof.
+do 3 rewrite <- subset_iff; intros.
+apply subset_trans with s'; auto.
+Qed.
+
+Lemma subset_equal: 
+ equal s s'=true -> subset s s'=true.
+Proof.
+auto with set.
+Qed.
+
+(** Properties of [choose] *)
+
+Lemma choose_mem_3: 
+ is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
+Proof.
+intros.
+generalize (@choose_1 s) (@choose_2 s).
+destruct (choose s);intros.
+exists e;auto with set.
+generalize (H1 (refl_equal None)); clear H1.
+intros; rewrite (is_empty_1 H1) in H; discriminate.
+Qed.
+
+Lemma choose_mem_4: choose empty=None.
+Proof.
+generalize (@choose_1 empty).
+case (@choose empty);intros;auto.
+elim (@empty_1 e); auto.
+Qed.
+
+(** Properties of [add] *)
+
+Lemma add_mem_3: 
+ mem y s=true -> mem y (add x s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_equal: 
+ mem x s=true -> equal (add x s) s=true.
+Proof.
+auto with set.
+Qed.
+
+(** Properties of [remove] *)
+
+Lemma remove_mem_3: 
+ mem y (remove x s)=true -> mem y s=true.
+Proof.
+rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
+Qed.
+
+Lemma remove_equal: 
+ mem x s=false -> equal (remove x s) s=true.
+Proof.
+intros; apply equal_1; apply remove_equal.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma add_remove: 
+ mem x s=true -> equal (add x (remove x s)) s=true.
+Proof.
+intros; apply equal_1; apply add_remove; auto with set.
+Qed.
+
+Lemma remove_add: 
+ mem x s=false -> equal (remove x (add x s)) s=true.
+Proof.
+intros; apply equal_1; apply remove_add; auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+(** Properties of [is_empty] *)
+
+Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
+Proof.
+intros; apply bool_1; split; intros.
+rewrite MP.cardinal_1; simpl; auto with set.
+assert (cardinal s = 0) by (apply zerob_true_elim; auto).
+auto with set.
+Qed.
+
+(** Properties of [singleton] *)
+
+Lemma singleton_mem_1: mem x (singleton x)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
+Proof.
+intros; rewrite singleton_b.
+unfold eqb; destruct (eq_dec x y); intuition.
+Qed.
+
+Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
+Proof.
+intros; apply singleton_1; auto with set.
+Qed.
+
+(** Properties of [union] *)
+
+Lemma union_sym:
+ equal (union s s') (union s' s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_subset_equal: 
+ subset s s'=true -> equal (union s s') s'=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_equal_1: 
+ equal s s'=true-> equal (union s s'') (union s' s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_equal_2: 
+ equal s' s''=true-> equal (union s s') (union s s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_assoc: 
+ equal (union (union s s') s'') (union s (union s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_union_singleton: 
+ equal (add x s) (union (singleton x) s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_add: 
+ equal (union (add x s) s') (add x (union s s'))=true.
+Proof.
+auto with set.
+Qed.
+
+(* caracterisation of [union] via [subset] *)
+
+Lemma union_subset_1: subset s (union s s')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_subset_2: subset s' (union s s')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_subset_3:
+ subset s s''=true -> subset s' s''=true -> 
+  subset (union s s') s''=true.
+Proof.
+intros; apply subset_1; apply union_subset_3; auto with set.
+Qed.
+
+(** Properties of [inter] *) 
+
+Lemma inter_sym: equal (inter s s') (inter s' s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_subset_equal: 
+ subset s s'=true -> equal (inter s s') s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_equal_1: 
+ equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_equal_2: 
+ equal s' s''=true -> equal (inter s s') (inter s s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_assoc: 
+ equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_inter_1: 
+ equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_inter_2: 
+ equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_add_1: mem x s'=true -> 
+ equal (inter (add x s) s') (add x (inter s s'))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_add_2: mem x s'=false -> 
+ equal (inter (add x s) s') (inter s s')=true.
+Proof.
+intros; apply equal_1; apply inter_add_2.
+rewrite not_mem_iff; auto.
+Qed.
+
+(* caracterisation of [union] via [subset] *)
+
+Lemma inter_subset_1: subset (inter s s') s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_subset_2: subset (inter s s') s'=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_subset_3:
+ subset s'' s=true -> subset s'' s'=true -> 
+  subset s'' (inter s s')=true.
+Proof.
+intros; apply subset_1; apply inter_subset_3; auto with set.
+Qed.
+
+(** Properties of [diff] *)
+
+Lemma diff_subset: subset (diff s s') s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma diff_subset_equal:
+ subset s s'=true -> equal (diff s s') empty=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma remove_inter_singleton: 
+ equal (remove x s) (diff s (singleton x))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma diff_inter_empty:
+ equal (inter (diff s s') (inter s s')) empty=true. 
+Proof.
+auto with set.
+Qed.
+
+Lemma diff_inter_all: 
+ equal (union (diff s s') (inter s s')) s=true.
+Proof.
+auto with set.
+Qed.
+
+End BasicProperties.
+
+Hint Immediate empty_mem is_empty_equal_empty add_mem_1
+   remove_mem_1 singleton_equal_add union_mem inter_mem
+   diff_mem equal_sym add_remove remove_add : set. 
+Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
+   choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
+   subset_refl subset_equal subset_antisym
+   add_mem_3 add_equal remove_mem_3 remove_equal : set.
+
+
+(** General recursion principle *)
+
+Lemma set_rec:  forall (P:t->Type),
+ (forall s s', equal s s'=true -> P s -> P s') -> 
+ (forall s x, mem x s=false -> P s -> P (add x s)) -> 
+ P empty -> forall s, P s.
+Proof.
+intros.
+apply set_induction; auto; intros.
+apply X with empty; auto with set.
+apply X with (add x s0); auto with set.
+apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto.
+apply X0; auto with set; apply mem_3; auto.
+Qed.
+
+(** Properties of [fold] *)
+
+Lemma exclusive_set : forall s s' x,
+ ~(In x s/\In x s') <-> mem x s && mem x s'=false.
+Proof.
+intros; do 2 rewrite mem_iff.
+destruct (mem x s); destruct (mem x s'); intuition.
+Qed.
+
+Section Fold. 
+Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
+Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
+Variables (i:A).
+Variables (s s':t)(x:elt).
+ 
+Lemma fold_empty: (fold f empty i) = i.
+Proof. 
+apply fold_empty; auto.
+Qed.
+
+Lemma fold_equal: 
+ equal s s'=true -> eqA (fold f s i) (fold f s' i).
+Proof. 
+intros; apply fold_equal with (eqA:=eqA); auto with set.
+Qed.
+   
+Lemma fold_add: 
+ mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
+Proof. 
+intros; apply fold_add with (eqA:=eqA); auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma add_fold: 
+  mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
+Proof.
+intros; apply add_fold with (eqA:=eqA); auto with set.
+Qed.
+
+Lemma remove_fold_1: 
+ mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
+Proof.
+intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
+Qed.
+
+Lemma remove_fold_2: 
+ mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
+Proof.
+intros; apply remove_fold_2 with (eqA:=eqA); auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma fold_union: 
+ (forall x, mem x s && mem x s'=false) -> 
+ eqA (fold f (union s s') i) (fold f s (fold f s' i)).
+Proof.
+intros; apply fold_union with (eqA:=eqA); auto.
+intros; rewrite exclusive_set; auto.
+Qed.
+
+End Fold.
+
+(** Properties of [cardinal] *)
+
+Lemma add_cardinal_1: 
+ forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_cardinal_2: 
+ forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
+Proof.
+intros; apply add_cardinal_2; auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma remove_cardinal_1: 
+ forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
+Proof.
+intros; apply remove_cardinal_1; auto with set.
+Qed.
+
+Lemma remove_cardinal_2: 
+ forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
+Proof.
+intros; apply Equal_cardinal; apply equal_2; auto with set.
+Qed.
+
+Lemma union_cardinal: 
+ forall s s', (forall x, mem x s && mem x s'=false) -> 
+ cardinal (union s s')=cardinal s+cardinal s'.
+Proof.
+intros; apply union_cardinal; auto; intros.
+rewrite exclusive_set; auto.
+Qed.
+
+Lemma subset_cardinal: 
+ forall s s', subset s s'=true -> cardinal s<=cardinal s'.
+Proof.
+intros; apply subset_cardinal; auto with set.
+Qed.
+
+Section Bool.
+
+(** Properties of [filter] *)
+
+Variable f:elt->bool.
+Variable Comp: compat_bool E.eq f.
+
+Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
+Proof.
+unfold compat_bool in *; intros; f_equal; auto.
+Qed.
+
+Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
+Proof. 
+intros; apply filter_b; auto.
+Qed.
+
+Lemma for_all_filter: 
+ forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
+Proof. 
+intros; apply bool_1; split; intros.
+apply is_empty_1.
+unfold Empty; intros. 
+rewrite filter_iff; auto.
+red; destruct 1.
+rewrite <- (@for_all_iff s f) in H; auto.
+rewrite (H a H0) in H1; discriminate.
+apply for_all_1; auto; red; intros.
+revert H; rewrite <- is_empty_iff.
+unfold Empty; intro H; generalize (H x); clear H.
+rewrite filter_iff; auto.
+destruct (f x); auto.
+Qed.
+
+Lemma exists_filter : 
+ forall s, exists_ f s=negb (is_empty (filter f s)).
+Proof. 
+intros; apply bool_1; split; intros. 
+destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).
+apply bool_6.
+red; intros; apply (@is_empty_2 _ H0 a); auto with set.
+generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)).
+destruct (choose (filter f s)).
+intros H0 _; apply exists_1; auto.
+exists e; generalize (H0 e); rewrite filter_iff; auto.
+intros _ H0.
+rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate.
+Qed.
+
+Lemma partition_filter_1: 
+ forall s, equal (fst (partition f s)) (filter f s)=true.
+Proof. 
+auto with set.
+Qed.
+
+Lemma partition_filter_2: 
+ forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
+Proof. 
+auto with set.
+Qed.
+
+Lemma filter_add_1 : forall s x, f x = true -> 
+ filter f (add x s) [=] add x (filter f s). 
+Proof.
+red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
+intuition.
+rewrite <- H; apply Comp; auto.
+Qed.
+
+Lemma filter_add_2 : forall s x, f x = false -> 
+ filter f (add x s) [=] filter f s. 
+Proof.
+red; intros; do 2 (rewrite filter_iff; auto); set_iff.
+intuition.
+assert (f x = f a) by (apply Comp; auto).
+rewrite H in H1; rewrite H2 in H1; discriminate.
+Qed.
+
+Lemma add_filter_1 : forall s s' x, 
+ f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
+Proof.
+unfold Add, MP.Add; intros.
+repeat rewrite filter_iff; auto.
+rewrite H0; clear H0.
+assert (E.eq x y -> f y = true) by 
+ (intro H0; rewrite <- (Comp _ _ H0); auto).
+tauto.
+Qed.
+
+Lemma add_filter_2 : forall s s' x, 
+ f x=false -> (Add x s s') -> filter f s [=] filter f s'.
+Proof.
+unfold Add, MP.Add, Equal; intros.
+repeat rewrite filter_iff; auto.
+rewrite H0; clear H0.
+assert (f a = true -> ~E.eq x a).
+ intros H0 H1.
+ rewrite (Comp _ _ H1) in H.
+ rewrite H in H0; discriminate.
+tauto. 
+Qed.
+
+Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
+  forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
+Proof.
+clear Comp' Comp f.
+intros.
+assert (compat_bool E.eq (fun x => orb (f x) (g x))).
+  unfold compat_bool; intros.
+  rewrite (H x y H1);  rewrite (H0 x y H1); auto.
+unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto.
+assert (f a || g a = true <-> f a = true \/ g a = true).
+  split; auto with bool.
+  intro H3; destruct (orb_prop _ _ H3); auto.
+tauto.
+Qed.
+
+Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').
+Proof.
+unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.
+Qed.
+
+(** Properties of [for_all] *)
+
+Lemma for_all_mem_1: forall s, 
+ (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
+Proof.
+intros.
+rewrite for_all_filter; auto.
+rewrite is_empty_equal_empty.
+apply equal_mem_1;intros.
+rewrite filter_b; auto.
+rewrite empty_mem.
+generalize (H a); case (mem a s);intros;auto.
+rewrite H0;auto.
+Qed.
+
+Lemma for_all_mem_2: forall s, 
+ (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true. 
+Proof.
+intros.
+rewrite for_all_filter in H; auto.
+rewrite is_empty_equal_empty in H.
+generalize (equal_mem_2 _ _ H x).
+rewrite filter_b; auto.
+rewrite empty_mem.
+rewrite H0; simpl;intros.
+replace true with (negb false);auto;apply negb_sym;auto.
+Qed.
+
+Lemma for_all_mem_3: 
+ forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
+Proof.
+intros.
+apply (bool_eq_ind (for_all f s));intros;auto.
+rewrite for_all_filter in H1; auto.
+rewrite is_empty_equal_empty in H1.
+generalize (equal_mem_2 _ _ H1 x).
+rewrite filter_b; auto.
+rewrite empty_mem.
+rewrite H.
+rewrite H0.
+simpl;auto.
+Qed.
+
+Lemma for_all_mem_4: 
+ forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
+Proof.
+intros.
+rewrite for_all_filter in H; auto.
+destruct (choose_mem_3 _ H) as (x,(H0,H1));intros.
+exists x.
+rewrite filter_b in H1; auto.
+elim (andb_prop _ _ H1).
+split;auto.
+replace false with (negb true);auto;apply negb_sym;auto.
+Qed.
+
+(** Properties of [exists] *)
+
+Lemma for_all_exists: 
+ forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
+Proof.
+intros.
+rewrite for_all_b; auto.
+rewrite exists_b; auto.
+induction (elements s); simpl; auto.
+destruct (f a); simpl; auto.
+Qed.
+
+End Bool.
+Section Bool'.
+
+Variable f:elt->bool.
+Variable Comp: compat_bool E.eq f.
+
+Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
+Proof.
+unfold compat_bool in *; intros; f_equal; auto.
+Qed.
+
+Lemma exists_mem_1: 
+ forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
+Proof.
+intros.
+rewrite for_all_exists; auto.
+rewrite for_all_mem_1;auto with bool.
+intros;generalize (H x H0);intros. 
+symmetry;apply negb_sym;simpl;auto.
+Qed.
+
+Lemma exists_mem_2: 
+ forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false. 
+Proof.
+intros.
+rewrite for_all_exists in H; auto.
+replace false with (negb true);auto;apply negb_sym;symmetry.
+rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
+replace true with (negb false);auto;apply negb_sym;auto.
+Qed.
+
+Lemma exists_mem_3: 
+ forall s x, mem x s=true -> f x=true -> exists_ f s=true.
+Proof.
+intros.
+rewrite for_all_exists; auto.
+symmetry;apply negb_sym;simpl.
+apply for_all_mem_3 with x;auto.
+rewrite H0;auto.
+Qed.
+
+Lemma exists_mem_4: 
+ forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
+Proof.
+intros.
+rewrite for_all_exists in H; auto.
+elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros.
+elim p;intros.
+exists x;split;auto.
+replace true with (negb false);auto;apply negb_sym;auto.
+replace false with (negb true);auto;apply negb_sym;auto.
+Qed.
+
+End Bool'.
+
+Section Sum.
+
+(** Adding a valuation function on all elements of a set. *)
+
+Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. 
+Notation compat_opL := (compat_op E.eq (@Logic.eq _)).
+Notation transposeL := (transpose (@Logic.eq _)).
+
+Lemma sum_plus : 
+  forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
+    forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
+Proof.
+unfold sum.
+intros f g Hf Hg.
+assert (fc : compat_opL (fun x:elt =>plus (f x))).  auto.
+assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
+assert (gc : compat_opL (fun x:elt => plus (g x))). auto.
+assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
+assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto.
+assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
+assert (st := gen_st nat).
+intros s;pattern s; apply set_rec.
+intros.
+rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
+rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H).
+rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto.
+intros; do 3 (rewrite (fold_add _ _ st);auto).
+rewrite H0;simpl;omega.
+do 3 rewrite fold_empty;auto.
+Qed.
+
+Lemma sum_filter : forall f, (compat_bool E.eq f) -> 
+  forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
+Proof.
+unfold sum; intros f Hf.
+assert (st := gen_st nat).
+assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))). 
+ red; intros.
+ rewrite (Hf x x' H); auto.
+assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
+ red; intros; omega.
+intros s;pattern s; apply set_rec.
+intros.
+change elt with E.t.
+rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H).
+rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto.
+intros; rewrite (fold_add _ _ st _ cc ct); auto.
+generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) .
+assert (~ In x (filter f s0)).
+ intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H.
+case (f x); simpl; intros.
+rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto.
+rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto.
+intros; rewrite fold_empty;auto.
+rewrite MP.cardinal_1; auto.
+unfold Empty; intros.
+rewrite filter_iff; auto; set_iff; tauto.
+Qed.
+
+Lemma fold_compat : 
+  forall (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA))
+  (f g:elt->A->A),
+  (compat_op E.eq eqA f) -> (transpose eqA f) -> 
+  (compat_op E.eq eqA g) -> (transpose eqA g) -> 
+  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> 
+  (eqA (fold f s i) (fold g s i)).
+Proof.
+intros A eqA st f g fc ft gc gt i.
+intro s; pattern s; apply set_rec; intros.
+trans_st (fold f s0 i).
+apply fold_equal with (eqA:=eqA); auto.
+rewrite equal_sym; auto.
+trans_st (fold g s0 i).
+apply H0; intros; apply H1; auto with set.
+elim  (equal_2 H x); auto with set; intros.
+apply fold_equal with (eqA:=eqA); auto with set.
+trans_st (f x (fold f s0 i)).
+apply fold_add with (eqA:=eqA); auto with set.
+trans_st (g x (fold f s0 i)); auto with set.
+trans_st (g x (fold g s0 i)); auto with set.
+sym_st; apply fold_add with (eqA:=eqA); auto.
+do 2 rewrite fold_empty; refl_st.
+Qed.
+
+Lemma sum_compat : 
+  forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
+  forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
+intros.
+unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto.
+red; intros; omega.
+red; intros; omega.
+Qed.
+
+End Sum.
+
+End WEqProperties.
+
+
+(** Now comes a special version dedicated to full sets. For this
+    one, only one argument [(M:S)] is necessary. *)
 
 Module EqProperties (M:S).
   Module D := OT_as_DT M.E.
-  Include FSetWeakEqProperties.EqProperties M D.
+  Include WEqProperties D M.
 End EqProperties.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index a433a9d04..2bf0c1cae 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -14,16 +14,491 @@
   facts are mainly the specifications of [FSetInterface.S] written using 
   different styles: equivalence and boolean equalities. 
   Moreover, we prove that [E.Eq] and [Equal] are setoid equalities.
-
-  We now simply reuse facts proved for weak sets (those without 
-  order on elements).
 *)
 
 Require Import DecidableTypeEx.
-Require Export FSetInterface.
-Require FSetWeakFacts.
+Require Export FSetInterface. 
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** First, a functor for Weak Sets. Since the signature [WS] includes
+    an EqualityType and not a stronger DecidableType, this functor 
+    should take two arguments in order to compensate this. *)
+
+Module WFacts (Import E : DecidableType)(Import M : WSfun E).
+
+Notation eq_dec := E.eq_dec.
+Definition eqb x y := if eq_dec x y then true else false.
+
+(** * Specifications written using equivalences *)
+
+Section IffSpec. 
+Variable s s' s'' : t.
+Variable x y z : elt.
+
+Lemma In_eq_iff : E.eq x y -> (In x s <-> In y s).
+Proof.
+split; apply In_1; auto.
+Qed.
+
+Lemma mem_iff : In x s <-> mem x s = true.
+Proof.
+split; [apply mem_1|apply mem_2].
+Qed.
+
+Lemma not_mem_iff : ~In x s <-> mem x s = false.
+Proof.
+rewrite mem_iff; destruct (mem x s); intuition.
+Qed.
+
+Lemma equal_iff : s[=]s' <-> equal s s' = true.
+Proof. 
+split; [apply equal_1|apply equal_2].
+Qed.
+
+Lemma subset_iff : s[<=]s' <-> subset s s' = true.
+Proof. 
+split; [apply subset_1|apply subset_2].
+Qed.
+
+Lemma empty_iff : In x empty <-> False.
+Proof.
+intuition; apply (empty_1 H).
+Qed.
+
+Lemma is_empty_iff : Empty s <-> is_empty s = true. 
+Proof. 
+split; [apply is_empty_1|apply is_empty_2].
+Qed.
+
+Lemma singleton_iff : In y (singleton x) <-> E.eq x y.
+Proof.
+split; [apply singleton_1|apply singleton_2].
+Qed.
+
+Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s.
+Proof. 
+split; [ | destruct 1; [apply add_1|apply add_2]]; auto.
+destruct (eq_dec x y) as [E|E]; auto.
+intro H; right; exact (add_3 E H).
+Qed.
+
+Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s)  <-> In y s).
+Proof.
+split; [apply add_3|apply add_2]; auto.
+Qed.
+
+Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y.
+Proof.
+split; [split; [apply remove_3 with x |] | destruct 1; apply remove_2]; auto.
+intro.
+apply (remove_1 H0 H).
+Qed.
+
+Lemma remove_neq_iff : ~ E.eq x y -> (In y (remove x s) <-> In y s).
+Proof.
+split; [apply remove_3|apply remove_2]; auto.
+Qed.
+
+Lemma union_iff : In x (union s s') <-> In x s \/ In x s'.
+Proof.
+split; [apply union_1 | destruct 1; [apply union_2|apply union_3]]; auto.
+Qed.
+
+Lemma inter_iff : In x (inter s s') <-> In x s /\ In x s'.
+Proof.
+split; [split; [apply inter_1 with s' | apply inter_2 with s] | destruct 1; apply inter_3]; auto.
+Qed.
+
+Lemma diff_iff : In x (diff s s') <-> In x s /\ ~ In x s'.
+Proof.
+split; [split; [apply diff_1 with s' | apply diff_2 with s] | destruct 1; apply diff_3]; auto.
+Qed.
+
+Variable f : elt->bool.
+
+Lemma filter_iff :  compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true).
+Proof. 
+split; [split; [apply filter_1 with f | apply filter_2 with s] | destruct 1; apply filter_3]; auto. 
+Qed.
+
+Lemma for_all_iff : compat_bool E.eq f ->
+  (For_all (fun x => f x = true) s <-> for_all f s = true).
+Proof.
+split; [apply for_all_1 | apply for_all_2]; auto.
+Qed.
+ 
+Lemma exists_iff : compat_bool E.eq f ->
+  (Exists (fun x => f x = true) s <-> exists_ f s = true).
+Proof.
+split; [apply exists_1 | apply exists_2]; auto.
+Qed.
+
+Lemma elements_iff : In x s <-> InA E.eq x (elements s).
+Proof. 
+split; [apply elements_1 | apply elements_2].
+Qed.
+
+End IffSpec.
+
+(** Useful tactic for simplifying expressions like [In y (add x (union s s'))] *)
+  
+Ltac set_iff := 
+ repeat (progress (
+  rewrite add_iff || rewrite remove_iff || rewrite singleton_iff 
+  || rewrite union_iff || rewrite inter_iff || rewrite diff_iff
+  || rewrite empty_iff)).
+
+(**  * Specifications written using boolean predicates *)
+
+Section BoolSpec.
+Variable s s' s'' : t.
+Variable x y z : elt.
+
+Lemma mem_b : E.eq x y -> mem x s = mem y s.
+Proof. 
+intros.
+generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H).
+destruct (mem x s); destruct (mem y s); intuition.
+Qed.
+
+Lemma empty_b : mem y empty = false.
+Proof.
+generalize (empty_iff y)(mem_iff empty y).
+destruct (mem y empty); intuition.
+Qed.
+
+Lemma add_b : mem y (add x s) = eqb x y || mem y s.
+Proof.
+generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb.
+destruct (eq_dec x y); destruct (mem y s); destruct (mem y (add x s)); intuition.
+Qed.
+
+Lemma add_neq_b : ~ E.eq x y -> mem y (add x s) = mem y s.
+Proof.
+intros; generalize (mem_iff (add x s) y)(mem_iff s y)(add_neq_iff s H).
+destruct (mem y s); destruct (mem y (add x s)); intuition.
+Qed.
+
+Lemma remove_b : mem y (remove x s) = mem y s && negb (eqb x y).
+Proof.
+generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_iff s x y); unfold eqb.
+destruct (eq_dec x y); destruct (mem y s); destruct (mem y (remove x s)); simpl; intuition.
+Qed.
+
+Lemma remove_neq_b : ~ E.eq x y -> mem y (remove x s) = mem y s.
+Proof.
+intros; generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_neq_iff s H).
+destruct (mem y s); destruct (mem y (remove x s)); intuition.
+Qed.
+
+Lemma singleton_b : mem y (singleton x) = eqb x y.
+Proof. 
+generalize (mem_iff (singleton x) y)(singleton_iff x y); unfold eqb.
+destruct (eq_dec x y); destruct (mem y (singleton x)); intuition.
+Qed.
+
+Lemma union_b : mem x (union s s') = mem x s || mem x s'.
+Proof.
+generalize (mem_iff (union s s') x)(mem_iff s x)(mem_iff s' x)(union_iff s s' x).
+destruct (mem x s); destruct (mem x s'); destruct (mem x (union s s')); intuition.
+Qed.
+
+Lemma inter_b : mem x (inter s s') = mem x s && mem x s'.
+Proof.
+generalize (mem_iff (inter s s') x)(mem_iff s x)(mem_iff s' x)(inter_iff s s' x).
+destruct (mem x s); destruct (mem x s'); destruct (mem x (inter s s')); intuition.
+Qed.
+
+Lemma diff_b : mem x (diff s s') = mem x s && negb (mem x s').
+Proof.
+generalize (mem_iff (diff s s') x)(mem_iff s x)(mem_iff s' x)(diff_iff s s' x).
+destruct (mem x s); destruct (mem x s'); destruct (mem x (diff s s')); simpl; intuition.
+Qed.
+
+Lemma elements_b : mem x s = existsb (eqb x) (elements s).
+Proof.
+generalize (mem_iff s x)(elements_iff s x)(existsb_exists (eqb x) (elements s)).
+rewrite InA_alt.
+destruct (mem x s); destruct (existsb (eqb x) (elements s)); auto; intros.
+symmetry.
+rewrite H1.
+destruct H0 as (H0,_).
+destruct H0 as (a,(Ha1,Ha2)); [ intuition |].
+exists a; intuition.
+unfold eqb; destruct (eq_dec x a); auto.
+rewrite <- H.
+rewrite H0.
+destruct H1 as (H1,_).
+destruct H1 as (a,(Ha1,Ha2)); [intuition|].
+exists a; intuition.
+unfold eqb in *; destruct (eq_dec x a); auto; discriminate.
+Qed.
+
+Variable f : elt->bool.
+
+Lemma filter_b : compat_bool E.eq f -> mem x (filter f s) = mem x s && f x.
+Proof. 
+intros.
+generalize (mem_iff (filter f s) x)(mem_iff s x)(filter_iff s x H).
+destruct (mem x s); destruct (mem x (filter f s)); destruct (f x); simpl; intuition.
+Qed.
+
+Lemma for_all_b : compat_bool E.eq f ->
+  for_all f s = forallb f (elements s).
+Proof.
+intros.
+generalize (forallb_forall f (elements s))(for_all_iff s H)(elements_iff s).
+unfold For_all.
+destruct (forallb f (elements s)); destruct (for_all f s); auto; intros.
+rewrite <- H1; intros.
+destruct H0 as (H0,_).
+rewrite (H2 x0) in H3.
+rewrite (InA_alt E.eq x0 (elements s)) in H3.
+destruct H3 as (a,(Ha1,Ha2)).
+rewrite (H _ _ Ha1).
+apply H0; auto.
+symmetry.
+rewrite H0; intros.
+destruct H1 as (_,H1).
+apply H1; auto.
+rewrite H2.
+rewrite InA_alt; eauto.
+Qed.
+
+Lemma exists_b : compat_bool E.eq f -> 
+  exists_ f s = existsb f (elements s).
+Proof.
+intros.
+generalize (existsb_exists f (elements s))(exists_iff s H)(elements_iff s).
+unfold Exists.
+destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros.
+rewrite <- H1; intros.
+destruct H0 as (H0,_).
+destruct H0 as (a,(Ha1,Ha2)); auto.
+exists a; split; auto.
+rewrite H2; rewrite InA_alt; eauto.
+symmetry.
+rewrite H0.
+destruct H1 as (_,H1).
+destruct H1 as (a,(Ha1,Ha2)); auto.
+rewrite (H2 a) in Ha1.
+rewrite (InA_alt E.eq a (elements s)) in Ha1.
+destruct Ha1 as (b,(Hb1,Hb2)).
+exists b; auto.
+rewrite <- (H _ _ Hb1); auto.
+Qed.
+
+End BoolSpec.
+
+(** * [E.eq] and [Equal] are setoid equalities *)
+
+Definition E_ST : Setoid_Theory elt E.eq.
+Proof.
+constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
+Qed.
+
+Definition Equal_ST : Setoid_Theory t Equal.
+Proof. 
+constructor; [apply eq_refl | apply eq_sym | apply eq_trans].
+Qed.
+
+Add Relation elt E.eq 
+ reflexivity proved by E.eq_refl 
+ symmetry proved by E.eq_sym
+ transitivity proved by E.eq_trans 
+ as EltSetoid.
+
+Add Relation t Equal 
+ reflexivity proved by eq_refl 
+ symmetry proved by eq_sym
+ transitivity proved by eq_trans 
+ as EqualSetoid.
+
+Add Morphism In with signature E.eq ==> Equal ==> iff as In_m.
+Proof.
+unfold Equal; intros x y H s s' H0.
+rewrite (In_eq_iff s H); auto.
+Qed.
+
+Add Morphism is_empty : is_empty_m.
+Proof.
+unfold Equal; intros s s' H.
+generalize (is_empty_iff s)(is_empty_iff s').
+destruct (is_empty s); destruct (is_empty s'); 
+ unfold Empty; auto; intros.
+symmetry.
+rewrite <- H1; intros a Ha.
+rewrite <- (H a) in Ha.
+destruct H0 as (_,H0).
+exact (H0 (refl_equal true) _ Ha).
+rewrite <- H0; intros a Ha.
+rewrite (H a) in Ha.
+destruct H1 as (_,H1).
+exact (H1 (refl_equal true) _ Ha).
+Qed.
+
+Add Morphism Empty with signature Equal ==> iff as Empty_m.
+Proof. 
+intros; do 2 rewrite is_empty_iff; rewrite H; intuition.
+Qed.
+
+Add Morphism mem : mem_m.
+Proof.
+unfold Equal; intros x y H s s' H0.
+generalize (H0 x); clear H0; rewrite (In_eq_iff s' H).
+generalize (mem_iff s x)(mem_iff s' y).
+destruct (mem x s); destruct (mem y s'); intuition.
+Qed.
+
+Add Morphism singleton : singleton_m.
+Proof.
+unfold Equal; intros x y H a.
+do 2 rewrite singleton_iff; split; intros.
+apply E.eq_trans with x; auto.
+apply E.eq_trans with y; auto.
+Qed.
+
+Add Morphism add : add_m.
+Proof.
+unfold Equal; intros x y H s s' H0 a.
+do 2 rewrite add_iff; rewrite H; rewrite H0; intuition.
+Qed.
+
+Add Morphism remove : remove_m.
+Proof.
+unfold Equal; intros x y H s s' H0 a.
+do 2 rewrite remove_iff; rewrite H; rewrite H0; intuition.
+Qed.
+
+Add Morphism union : union_m.
+Proof.
+unfold Equal; intros s s' H s'' s''' H0 a.
+do 2 rewrite union_iff; rewrite H; rewrite H0; intuition.
+Qed.
+
+Add Morphism inter : inter_m.
+Proof.
+unfold Equal; intros s s' H s'' s''' H0 a.
+do 2 rewrite inter_iff; rewrite H; rewrite H0; intuition.
+Qed.
+
+Add Morphism diff : diff_m.
+Proof.
+unfold Equal; intros s s' H s'' s''' H0 a.
+do 2 rewrite diff_iff; rewrite H; rewrite H0; intuition.
+Qed.
+
+Add Morphism Subset with signature Equal ==> Equal ==> iff as  Subset_m.
+Proof. 
+unfold Equal, Subset; firstorder.
+Qed.
+
+Add Morphism subset : subset_m.
+Proof.
+intros s s' H s'' s''' H0.
+generalize (subset_iff s s'') (subset_iff s' s'''). 
+destruct (subset s s''); destruct (subset s' s'''); auto; intros.
+rewrite H in H1; rewrite H0 in H1; intuition.
+rewrite H in H1; rewrite H0 in H1; intuition.
+Qed.
+
+Add Morphism equal : equal_m.
+Proof.
+intros s s' H s'' s''' H0.
+generalize (equal_iff s s'') (equal_iff s' s''').
+destruct (equal s s''); destruct (equal s' s'''); auto; intros.
+rewrite H in H1; rewrite H0 in H1; intuition.
+rewrite H in H1; rewrite H0 in H1; intuition.
+Qed.
+
+
+(* [Subset] is a setoid order *)
+
+Lemma Subset_refl : forall s, s[<=]s.
+Proof. red; auto. Defined.
+
+Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''.
+Proof. unfold Subset; eauto. Defined.
+
+Add Relation t Subset 
+ reflexivity proved by Subset_refl
+ transitivity proved by Subset_trans
+ as SubsetSetoid.
+(* NB: for the moment, it is important to use Defined and not Qed in 
+   the two previous lemmas, in order to allow conversion of 
+   SubsetSetoid coming from separate Facts modules. See bug #1738. *)
+
+Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m.
+Proof.
+unfold Subset, impl; intros; eauto with set.
+Qed.
+
+Add Morphism Empty with signature Subset --> impl as Empty_s_m.
+Proof. 
+unfold Subset, Empty, impl; firstorder.
+Qed.
+
+Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m.
+Proof.
+unfold Subset; intros x y H s s' H0 a.
+do 2 rewrite add_iff; rewrite H; intuition.
+Qed.
+
+Add Morphism remove with signature E.eq ==> Subset ++> Subset as remove_s_m.
+Proof.
+unfold Subset; intros x y H s s' H0 a.
+do 2 rewrite remove_iff; rewrite H; intuition.
+Qed.
+
+Add Morphism union with signature Subset ++> Subset ++> Subset as union_s_m.
+Proof.
+unfold Equal; intros s s' H s'' s''' H0 a.
+do 2 rewrite union_iff; intuition.
+Qed.
+
+Add Morphism inter with signature Subset ++> Subset ++> Subset as inter_s_m.
+Proof.
+unfold Equal; intros s s' H s'' s''' H0 a.
+do 2 rewrite inter_iff; intuition.
+Qed.
+
+Add Morphism diff with signature Subset ++> Subset --> Subset as diff_s_m.
+Proof.
+unfold Subset; intros s s' H s'' s''' H0 a.
+do 2 rewrite diff_iff; intuition.
+Qed.
+
+(* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism
+   without additional hypothesis on [f]. For instance: *)
+
+Lemma filter_equal : forall f, compat_bool E.eq f -> 
+  forall s s', s[=]s' -> filter f s [=] filter f s'.
+Proof.
+unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto.
+Qed.
+
+Lemma filter_subset : forall f, compat_bool E.eq f -> 
+  forall s s', s[<=]s' -> filter f s [<=] filter f s'.
+Proof.
+unfold Subset; intros; rewrite filter_iff in *; intuition.
+Qed.
+
+(* For [elements], [min_elt], [max_elt] and [choose], we would need setoid 
+   structures on [list elt] and [option elt]. *)
+
+(* Later:
+Add Morphism cardinal ; cardinal_m.
+*)
+
+End WFacts.
+
+
+(** Now comes a special version dedicated to full sets. For this 
+    one, only one argument [(M:S)] is necessary. *)
 
 Module Facts (M:S).
- Module D:=OT_as_DT M.E.
- Include FSetWeakFacts.Facts M D.
+  Module D:=OT_as_DT M.E.
+  Include WFacts D M.
 End Facts.
+
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index f701dcf12..3ae983641 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -12,18 +12,28 @@
 
 (** Set interfaces *)
 
-Require Export Bool OrderedType.
+Require Export Bool OrderedType DecidableType.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** * Non-dependent signature
+(** * Non-dependent signatures
 
-    Signature [S] presents sets as purely informative programs 
-    together with axioms *)
+    The following signatures presents sets as purely informative 
+    programs together with axioms *)
 
-Module Type S.
 
-  Declare Module E : OrderedType.
+
+(** ** Functorial signature for weak sets
+
+    Weak sets are sets without ordering on base elements, only 
+    a decidable equality. *)
+
+Module Type WSfun (E : EqualityType).
+
+  (** The module E of base objects is meant to be a DecidableType
+     (and used to be so). But requiring only an EqualityType here
+     allows subtyping between FSet and FSetWeak *)
+
   Definition elt := E.t.
 
   Parameter t : Set. (** the abstract type of sets *)
@@ -69,10 +79,10 @@ Module Type S.
   (** Set difference. *)
 
   Definition eq : t -> t -> Prop := Equal.
-  Parameter lt : t -> t -> Prop.
-  Parameter compare : forall s s' : t, Compare lt eq s s'.
-  (** Total ordering between sets. Can be used as the ordering function
-  for doing sets of sets. *)
+  (** EqualityType is a subset of this interface, but not 
+  DecidableType, in order to have FSetWeak < FSet. 
+  Hence no weak sets of weak sets in general, but it works 
+  at least with FSetWeakList.make that provides an eq_dec. *)
 
   Parameter equal : t -> t -> bool.
   (** [equal s1 s2] tests whether the sets [s1] and [s2] are
@@ -90,7 +100,9 @@ Module Type S.
 
   Parameter fold : forall A : Type, (elt -> A -> A) -> t -> A -> A.
   (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
-  where [x1 ... xN] are the elements of [s], in increasing order. *)
+  where [x1 ... xN] are the elements of [s].
+  The order in which elements of [s] are presented to [f] is
+  unspecified. *)
 
   Parameter for_all : (elt -> bool) -> t -> bool.
   (** [for_all p s] checks if all elements of the set
@@ -115,56 +127,38 @@ Module Type S.
   (** Coq comment: nat instead of int ... *)
 
   Parameter elements : t -> list elt.
-  (** Return the list of all elements of the given set.
-  The returned list is sorted in increasing order with respect
-  to the ordering [Ord.compare], where [Ord] is the argument
-  given to {!Set.Make}. *)
-
-  Parameter min_elt : t -> option elt.
-  (** Return the smallest element of the given set
-  (with respect to the [Ord.compare] ordering), or raise
-  [Not_found] if the set is empty. *)
-  (** Coq comment: [Not_found] is represented by the option type *)
-
-  Parameter max_elt : t -> option elt.
-  (** Same as {!Set.S.min_elt}, but returns the largest element of the
-  given set. *)
-  (** Coq comment: [Not_found] is represented by the option type *)
+  (** Return the list of all elements of the given set, in any order. *)
 
   Parameter choose : t -> option elt.
   (** Return one element of the given set, or raise [Not_found] if
-  the set is empty. Which element is chosen is unspecified,
-  but equal elements will be chosen for equal sets. *)
+  the set is empty. Which element is chosen is unspecified.
+  Equal sets could return different elements. *)
   (** Coq comment: [Not_found] is represented by the option type *)
 
   Section Spec. 
 
-  Variable s s' s'' : t.
+  Variable s s' s'': t.
   Variable x y : elt.
 
   (** Specification of [In] *)
   Parameter In_1 : E.eq x y -> In x s -> In y s.
- 
+
   (** Specification of [eq] *)
   Parameter eq_refl : eq s s. 
   Parameter eq_sym : eq s s' -> eq s' s.
   Parameter eq_trans : eq s s' -> eq s' s'' -> eq s s''.
- 
-  (** Specification of [lt] *)
-  Parameter lt_trans : lt s s' -> lt s' s'' -> lt s s''.
-  Parameter lt_not_eq : lt s s' -> ~ eq s s'.
 
   (** Specification of [mem] *)
   Parameter mem_1 : In x s -> mem x s = true.
   Parameter mem_2 : mem x s = true -> In x s. 
  
   (** Specification of [equal] *) 
-  Parameter equal_1 : s[=]s' -> equal s s' = true.
-  Parameter equal_2 : equal s s' = true ->s[=]s'.
+  Parameter equal_1 : Equal s s' -> equal s s' = true.
+  Parameter equal_2 : equal s s' = true -> Equal s s'.
 
   (** Specification of [subset] *)
-  Parameter subset_1 : s[<=]s' -> subset s s' = true.
-  Parameter subset_2 : subset s s' = true -> s[<=]s'.
+  Parameter subset_1 : Subset s s' -> subset s s' = true.
+  Parameter subset_2 : subset s s' = true -> Subset s s'.
 
   (** Specification of [empty] *)
   Parameter empty_1 : Empty empty.
@@ -236,21 +230,90 @@ Module Type S.
       exists_ f s = true -> Exists (fun x => f x = true) s.
 
   (** Specification of [partition] *)
-  Parameter partition_1 : compat_bool E.eq f -> 
-      fst (partition f s) [=] filter f s.
-  Parameter partition_2 : compat_bool E.eq f -> 
-      snd (partition f s) [=] filter (fun x => negb (f x)) s.
+  Parameter partition_1 :
+      compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
+  Parameter partition_2 :
+      compat_bool E.eq f ->
+      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
 
   End Filter.
 
   (** Specification of [elements] *)
   Parameter elements_1 : In x s -> InA E.eq x (elements s).
   Parameter elements_2 : InA E.eq x (elements s) -> In x s.
-  Parameter elements_3 : sort E.lt (elements s).  
-  (* We add artificially elements_3w, a weaker version of 
-     elements_3, for allowing FSetWeak < FSet subtyping. *)
+  (** When compared with ordered FSet, here comes the only 
+      property that is really weaker: *)
   Parameter elements_3w : NoDupA E.eq (elements s).
 
+  (** Specification of [choose] *)
+  Parameter choose_1 : choose s = Some x -> In x s.
+  Parameter choose_2 : choose s = None -> Empty s.
+
+  End Spec.
+
+  Hint Resolve mem_1 equal_1 subset_1 empty_1
+    is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
+    remove_2 singleton_2 union_1 union_2 union_3
+    inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
+    partition_1 partition_2 elements_1 elements_3w 
+    : set.
+  Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
+    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
+    filter_1 filter_2 for_all_2 exists_2 elements_2 
+    : set.
+
+End WSfun.
+
+
+
+(** ** Static signature for weak sets
+
+    Similar to the functorial signature [SW], except that the 
+    module [E] of base elements is incorporated in the signature. *)
+
+Module Type WS.
+  Declare Module E : EqualityType.
+  Include Type WSfun E.
+End WS.
+
+
+
+(** ** Functorial signature for full sets
+
+    Based on [WSfun], plus ordering on sets and [min_elt] and [max_elt]
+    and some stronger specifications for other functions. *)
+
+Module Type Sfun (E : OrderedType).
+  Include Type WSfun E.
+
+  Parameter lt : t -> t -> Prop.
+  Parameter compare : forall s s' : t, Compare lt eq s s'.
+  (** Total ordering between sets. Can be used as the ordering function
+  for doing sets of sets. *)
+
+  Parameter min_elt : t -> option elt.
+  (** Return the smallest element of the given set
+  (with respect to the [Ord.compare] ordering), or raise
+  [Not_found] if the set is empty. *)
+  (** Coq comment: [Not_found] is represented by the option type *)
+
+  Parameter max_elt : t -> option elt.
+  (** Same as {!Set.S.min_elt}, but returns the largest element of the
+  given set. *)
+  (** Coq comment: [Not_found] is represented by the option type *)
+
+  Section Spec. 
+
+  Variable s s' s'' : t.
+  Variable x y : elt.
+ 
+  (** Specification of [lt] *)
+  Parameter lt_trans : lt s s' -> lt s' s'' -> lt s s''.
+  Parameter lt_not_eq : lt s s' -> ~ eq s s'.
+
+  (** Additionnal specification of [elements] *)
+  Parameter elements_3 : sort E.lt (elements s).  
+
   (** Specification of [min_elt] *)
   Parameter min_elt_1 : min_elt s = Some x -> In x s. 
   Parameter min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. 
@@ -261,9 +324,7 @@ Module Type S.
   Parameter max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. 
   Parameter max_elt_3 : max_elt s = None -> Empty s.
 
-  (** Specification of [choose] *)
-  Parameter choose_1 : choose s = Some x -> In x s.
-  Parameter choose_2 : choose s = None -> Empty s.
+  (** Additionnal specification of [choose] *)
   Parameter choose_equal: (equal s s')=true -> 
      match choose s, choose s' with  
       | Some x, Some x' => E.eq x x'
@@ -273,31 +334,42 @@ Module Type S.
 
   End Spec.
 
-  Hint Resolve mem_1 equal_1 subset_1 empty_1
-    is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
-    remove_2 singleton_2 union_1 union_2 union_3
-    inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
-    partition_1 partition_2 elements_1 elements_3
-    : set.
-  Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
-    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
-    filter_1 filter_2 for_all_2 exists_2 elements_2
-    min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3
-    : set.
-  (** for compatibility with earlier hints *)
-  Hint Resolve mem_2 equal_2 subset_2 is_empty_2 add_3
-    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
-    filter_1 filter_2 for_all_2 exists_2 elements_2
-    min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3
-    : oldset.
-  
- 
+  Hint Resolve elements_3 : set.
+  Hint Immediate 
+    min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 : set.
+
+End Sfun.
+
+
+(** ** Static signature for full sets
 
+    Similar to the functorial signature [Sfun], except that the 
+    module [E] of base elements is incorporated in the signature. *)
+
+Module Type S.
+  Declare Module E : OrderedType.
+  Include Type Sfun E.
 End S.
 
+
+(** ** Some subtyping tests
+
+WSfun ---> WS
+ |         |
+ |         |
+ V         V
+Sfun  ---> S 
+
+Module S_WS (M : S) <: SW := M.
+Module Sfun_WSfun (E:OrderedType)(M : Sfun E) <: WSfun E := M.
+Module S_Sfun (E:OrderedType)(M : S with Module E:=E) <: Sfun E := M.
+Module WS_WSfun (E:EqualityType)(M : WS with Module E:=E) <: WSfun E := M.
+*)
+
+
 (** * Dependent signature 
 
-    Signature [Sdep] presents sets using dependent types *)
+    Signature [Sdep] presents full sets using dependent types *)
 
 Module Type Sdep.
 
@@ -427,7 +499,8 @@ Module Type Sdep.
      match choose s, choose s' with 
        | inleft (exist x _), inleft (exist x' _) => E.eq x x'
        | inright _, inright _  => True
-       | _, _                        => False
+       | _, _  => False
      end.
 
 End Sdep.
+
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index dd24d29b4..5525c3ecc 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -16,26 +16,771 @@
     [In x s] instead of [mem x s=true], 
     [Equal s s'] instead of [equal s s'=true], etc. *)
 
-Require Export FSetInterface. 
+Require Export FSetInterface.
 Require Import DecidableTypeEx FSetFacts FSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Hint Unfold transpose compat_op compat_nat.
+Hint Unfold transpose compat_op.
 Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence.
 
-(** First, the properties that do not rely on the element ordering 
-    are imported verbatim from FSetWeakProperties *)
+(** First, a functor for Weak Sets. Since the signature [WS] includes
+    an EqualityType and not a stronger DecidableType, this functor
+    should take two arguments in order to compensate this. *)
 
-Require FSetWeakProperties.
+Module WProperties (Import E : DecidableType)(M : WSfun E).
+  Module Import FM := WFacts E M.
+  Module Import Dec := WDecide E M.
+  Import M.
+
+  Lemma In_dec : forall x s, {In x s} + {~ In x s}.
+  Proof.
+  intros; generalize (mem_iff s x); case (mem x s); intuition.
+  Qed.
+
+  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
+
+  Lemma Add_Equal : forall x s s', Add x s s' <-> s' [=] add x s.
+  Proof.
+  unfold Add.
+  split; intros.
+  red; intros.
+  rewrite H; clear H.
+  fsetdec.
+  fsetdec.
+  Qed.
+  
+  Ltac expAdd := repeat rewrite Add_Equal.
+
+  Section BasicProperties.
+
+  Variable s s' s'' s1 s2 s3 : t.
+  Variable x x' : elt.
+
+  Lemma equal_refl : s[=]s.
+  Proof. fsetdec. Qed.
+
+  Lemma equal_sym : s[=]s' -> s'[=]s.
+  Proof. fsetdec. Qed.
+
+  Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3.
+  Proof. fsetdec. Qed.
+
+  Lemma subset_refl : s[<=]s. 
+  Proof. fsetdec. Qed.
+
+  Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
+  Proof. fsetdec. Qed.
+
+  Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
+  Proof. fsetdec. Qed.
+
+  Lemma subset_equal : s[=]s' -> s[<=]s'.
+  Proof. fsetdec. Qed.
+
+  Lemma subset_empty : empty[<=]s.
+  Proof. fsetdec. Qed.
+
+  Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2.
+  Proof. fsetdec. Qed.
+
+  Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3.
+  Proof. fsetdec. Qed.
+ 
+  Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2.
+  Proof. fsetdec. Qed.
+
+  Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2.
+  Proof. fsetdec. Qed.
+
+  Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.
+  Proof. fsetdec. Qed.
+ 
+  Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
+  Proof. intuition fsetdec. Qed.
+
+  Lemma empty_is_empty_1 : Empty s -> s[=]empty.
+  Proof. fsetdec. Qed.
+
+  Lemma empty_is_empty_2 : s[=]empty -> Empty s.
+  Proof. fsetdec. Qed.
+
+  Lemma add_equal : In x s -> add x s [=] s.
+  Proof. fsetdec. Qed.
+ 
+  Lemma add_add : add x (add x' s) [=] add x' (add x s).
+  Proof. fsetdec. Qed.
+
+  Lemma remove_equal : ~ In x s -> remove x s [=] s.
+  Proof. fsetdec. Qed.
+
+  Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.
+  Proof. fsetdec. Qed.
+
+  Lemma add_remove : In x s -> add x (remove x s) [=] s.
+  Proof. fsetdec. Qed.
+
+  Lemma remove_add : ~In x s -> remove x (add x s) [=] s.
+  Proof. fsetdec. Qed.
+
+  Lemma singleton_equal_add : singleton x [=] add x empty.
+  Proof. fsetdec. Qed.
+
+  Lemma union_sym : union s s' [=] union s' s.
+  Proof. fsetdec. Qed.
+
+  Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'.
+  Proof. fsetdec. Qed.
+
+  Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.
+  Proof. fsetdec. Qed.
+
+  Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.
+  Proof. fsetdec. Qed.
+
+  Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
+  Proof. fsetdec. Qed.
+
+  Lemma add_union_singleton : add x s [=] union (singleton x) s.
+  Proof. fsetdec. Qed.
+
+  Lemma union_add : union (add x s) s' [=] add x (union s s').
+  Proof. fsetdec. Qed.
+
+  Lemma union_remove_add_1 : 
+   union (remove x s) (add x s') [=] union (add x s) (remove x s').
+  Proof. fsetdec. Qed.
+
+  Lemma union_remove_add_2 : In x s -> 
+   union (remove x s) (add x s') [=] union s s'.
+  Proof. fsetdec. Qed.
+
+  Lemma union_subset_1 : s [<=] union s s'.
+  Proof. fsetdec. Qed.
+
+  Lemma union_subset_2 : s' [<=] union s s'.
+  Proof. fsetdec. Qed.
+
+  Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''.
+  Proof. fsetdec. Qed.
+
+  Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.
+  Proof. fsetdec. Qed. 
+
+  Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.
+  Proof. fsetdec. Qed. 
+
+  Lemma empty_union_1 : Empty s -> union s s' [=] s'.
+  Proof. fsetdec. Qed.
+
+  Lemma empty_union_2 : Empty s -> union s' s [=] s'.
+  Proof. fsetdec. Qed.
+
+  Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s'). 
+  Proof. fsetdec. Qed.
+
+  Lemma inter_sym : inter s s' [=] inter s' s.
+  Proof. fsetdec. Qed.
+
+  Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s.
+  Proof. fsetdec. Qed.
+
+  Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.
+  Proof. fsetdec. Qed.
+
+  Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.
+  Proof. fsetdec. Qed.
+
+  Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
+  Proof. fsetdec. Qed.
+
+  Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s'').
+  Proof. fsetdec. Qed.
+
+  Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s'').
+  Proof. fsetdec. Qed.
+
+  Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s').
+  Proof. fsetdec. Qed.
+
+  Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'.
+  Proof. fsetdec. Qed.
+
+  Lemma empty_inter_1 : Empty s -> Empty (inter s s').
+  Proof. fsetdec. Qed.
+
+  Lemma empty_inter_2 : Empty s' -> Empty (inter s s').
+  Proof. fsetdec. Qed.
+
+  Lemma inter_subset_1 : inter s s' [<=] s.
+  Proof. fsetdec. Qed.
+
+  Lemma inter_subset_2 : inter s s' [<=] s'.
+  Proof. fsetdec. Qed.
+
+  Lemma inter_subset_3 :
+   s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'.
+  Proof. fsetdec. Qed.
+
+  Lemma empty_diff_1 : Empty s -> Empty (diff s s'). 
+  Proof. fsetdec. Qed.
+
+  Lemma empty_diff_2 : Empty s -> diff s' s [=] s'.
+  Proof. fsetdec. Qed.
+
+  Lemma diff_subset : diff s s' [<=] s.
+  Proof. fsetdec. Qed.
+
+  Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty.
+  Proof. fsetdec. Qed.
+
+  Lemma remove_diff_singleton :
+   remove x s [=] diff s (singleton x).
+  Proof. fsetdec. Qed.
+
+  Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty. 
+  Proof. fsetdec. Qed.
+
+  Lemma diff_inter_all : union (diff s s') (inter s s') [=] s.
+  Proof. fsetdec. Qed.
+
+  Lemma Add_add : Add x s (add x s).
+  Proof. expAdd; fsetdec. Qed.
+
+  Lemma Add_remove : In x s -> Add x (remove x s) s. 
+  Proof. expAdd; fsetdec. Qed.
+
+  Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s'').
+  Proof. expAdd; fsetdec. Qed. 
+
+  Lemma inter_Add :
+   In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'').
+  Proof. expAdd; fsetdec. Qed. 
+
+  Lemma union_Equal :
+   In x s'' -> Add x s s' -> union s s'' [=] union s' s''.
+  Proof. expAdd; fsetdec. Qed. 
+
+  Lemma inter_Add_2 :
+   ~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''.
+  Proof. expAdd; fsetdec. Qed.
+
+  End BasicProperties.
+
+  Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
+  Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym 
+    subset_trans subset_empty subset_remove_3 subset_diff subset_add_3 
+    subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
+    remove_equal singleton_equal_add union_subset_equal union_equal_1 
+    union_equal_2 union_assoc add_union_singleton union_add union_subset_1 
+    union_subset_2 union_subset_3 inter_subset_equal inter_equal_1 inter_equal_2
+    inter_assoc union_inter_1 union_inter_2 inter_add_1 inter_add_2
+    empty_inter_1 empty_inter_2 empty_union_1 empty_union_2 empty_diff_1 
+    empty_diff_2 union_Add inter_Add union_Equal inter_Add_2 not_in_union 
+    inter_subset_1 inter_subset_2 inter_subset_3 diff_subset diff_subset_equal 
+    remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
+    Equal_remove add_add : set.
+
+  (** * Properties of elements *)
+
+  Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
+  Proof.
+  intros.
+  unfold Empty.
+  split; intros.
+  assert (forall a, ~ List.In a (elements s)).
+   red; intros.
+   apply (H a).
+   rewrite elements_iff.
+   rewrite InA_alt; exists a; auto.
+  destruct (elements s); auto.
+  elim (H0 e); simpl; auto.
+  red; intros.
+  rewrite elements_iff in H0.
+  rewrite InA_alt in H0; destruct H0.
+  rewrite H in H0; destruct H0 as (_,H0); inversion H0.
+  Qed.
+
+  (** * Alternative (weaker) specifications for [fold] *)
+
+  Section Old_Spec_Now_Properties. 
+
+  Notation NoDup := (NoDupA E.eq).
+
+  (** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
+        takes the set elements was unspecified. This specification reflects this fact: 
+  *)
+
+  Lemma fold_0 : 
+      forall s (A : Set) (i : A) (f : elt -> A -> A),
+      exists l : list elt,
+        NoDup l /\
+        (forall x : elt, In x s <-> InA E.eq x l) /\
+        fold f s i = fold_right f i l.
+  Proof.
+  intros; exists (rev (elements s)); split.
+  apply NoDupA_rev; auto with set.
+  exact E.eq_trans.
+  split; intros.
+  rewrite elements_iff; do 2 rewrite InA_alt.
+  split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
+  rewrite fold_left_rev_right.
+  apply fold_1.
+  Qed.
+
+  (** An alternate (and previous) specification for [fold] was based on 
+      the recursive structure of a set. It is now lemmas [fold_1] and 
+      [fold_2]. *)
+
+  Lemma fold_1 :
+   forall s (A : Set) (eqA : A -> A -> Prop) 
+     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+   Empty s -> eqA (fold f s i) i.
+  Proof.
+  unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))).
+  rewrite H3; clear H3.
+  generalize H H2; clear H H2; case l; simpl; intros.
+  refl_st.
+  elim (H e).
+  elim (H2 e); intuition. 
+  Qed.
+
+  Lemma fold_2 :
+   forall s s' x (A : Set) (eqA : A -> A -> Prop)
+     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+   compat_op E.eq eqA f ->
+   transpose eqA f ->
+   ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
+  Proof.
+  intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); 
+    destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
+  rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
+  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
+  eauto.
+  rewrite <- Hl1; auto.
+  intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1; 
+   rewrite (H2 a); intuition.
+  Qed.
+
+  (** In fact, [fold] on empty sets is more than equivalent to 
+      the initial element, it is Leibniz-equal to it. *)
+
+  Lemma fold_1b :
+   forall s (A : Set)(i : A) (f : elt -> A -> A),
+   Empty s -> (fold f s i) = i.
+  Proof.
+  intros.
+  rewrite M.fold_1.
+  rewrite elements_Empty in H; rewrite H; simpl; auto.
+  Qed.
+
+  (** Similar specifications for [cardinal]. *)
+
+  Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
+  Proof.
+  intros; rewrite cardinal_1; rewrite M.fold_1.
+  symmetry; apply fold_left_length; auto.
+  Qed.
+
+  Lemma cardinal_0 :
+     forall s, exists l : list elt,
+        NoDupA E.eq l /\
+        (forall x : elt, In x s <-> InA E.eq x l) /\ 
+        cardinal s = length l.
+  Proof. 
+  intros; exists (elements s); intuition; apply cardinal_1.
+  Qed.
+
+  Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
+  Proof.
+  intros; rewrite cardinal_fold; apply fold_1; auto.
+  Qed.
+
+  Lemma cardinal_2 :
+    forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).
+  Proof.
+  intros; do 2 rewrite cardinal_fold.
+  change S with ((fun _ => S) x).
+  apply fold_2; auto.
+  Qed.
+
+  End Old_Spec_Now_Properties.
+
+  (** * Induction principle over sets *)
+
+  Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
+  Proof.
+  intros.
+  rewrite elements_Empty, M.cardinal_1.
+  destruct (elements s); intuition; discriminate.
+  Qed.
+
+  Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s. 
+  Proof.
+  intros; rewrite cardinal_Empty; auto. 
+  Qed.
+  Hint Resolve cardinal_inv_1.
+ 
+  Lemma cardinal_inv_2 :
+   forall s n, cardinal s = S n -> { x : elt | In x s }.
+  Proof. 
+  intros; rewrite M.cardinal_1 in H.
+  generalize (elements_2 (s:=s)).
+  destruct (elements s); try discriminate. 
+  exists e; auto.
+  Qed.
+
+  Lemma cardinal_inv_2b :
+   forall s, cardinal s <> 0 -> { x : elt | In x s }.
+  Proof.
+  intro; generalize (@cardinal_inv_2 s); destruct cardinal; 
+   [intuition|eauto].
+  Qed.
+
+  Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
+  Proof. 
+  symmetry.
+  remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H.
+  induction n; intros.
+  apply cardinal_1; rewrite <- H; auto.
+  destruct (cardinal_inv_2 Heqn) as (x,H2).
+  revert Heqn.
+  rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.
+  rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set.
+  Qed.    
+
+  Add Morphism cardinal : cardinal_m.
+  Proof.
+  exact Equal_cardinal.
+  Qed.
+
+  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
+
+  Lemma set_induction :
+   forall P : t -> Type,
+   (forall s : t, Empty s -> P s) ->
+   (forall s s' : t, P s -> forall x : elt, ~In x s -> Add x s s' -> P s') ->
+   forall s : t, P s.
+  Proof.
+  intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
+  destruct (cardinal_inv_2 (sym_eq Heqn)) as (x,H0). 
+  apply X0 with (remove x s) x; auto with set.
+  apply IHn; auto.
+  assert (S n = S (cardinal (remove x s))).
+    rewrite Heqn; apply cardinal_2 with x; auto with set.
+  inversion H; auto.
+  Qed.
+
+  (** Other properties of [fold]. *)
+
+  Section Fold. 
+  Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
+  Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
+
+  Section Fold_1. 
+  Variable i i':A.
+
+  Lemma fold_empty : (fold f empty i) = i.
+  Proof. 
+  apply fold_1b; auto with set.
+  Qed.
+
+  Lemma fold_equal : 
+   forall s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
+  Proof. 
+  intros s; pattern s; apply set_induction; clear s; intros.
+  trans_st i.
+  apply fold_1; auto.
+  sym_st; apply fold_1; auto.
+  rewrite <- H0; auto.
+  trans_st (f x (fold f s i)).
+  apply fold_2 with (eqA := eqA); auto.
+  sym_st; apply fold_2 with (eqA := eqA); auto.
+  unfold Add in *; intros.
+  rewrite <- H2; auto.
+  Qed.
+   
+  Lemma fold_add : forall s x, ~In x s -> 
+   eqA (fold f (add x s) i) (f x (fold f s i)).
+  Proof. 
+  intros; apply fold_2 with (eqA := eqA); auto.
+  Qed.
+
+  Lemma add_fold : forall s x, In x s -> 
+   eqA (fold f (add x s) i) (fold f s i).
+  Proof.
+  intros; apply fold_equal; auto with set.
+  Qed.
+
+  Lemma remove_fold_1: forall s x, In x s -> 
+   eqA (f x (fold f (remove x s) i)) (fold f s i).
+  Proof.
+  intros.
+  sym_st.
+  apply fold_2 with (eqA:=eqA); auto with set.
+  Qed.
+
+  Lemma remove_fold_2: forall s x, ~In x s -> 
+   eqA (fold f (remove x s) i) (fold f s i).
+  Proof.
+  intros.
+  apply fold_equal; auto with set.
+  Qed.
+
+  Lemma fold_commutes : forall s x, 
+   eqA (fold f s (f x i)) (f x (fold f s i)).
+  Proof.
+  intros; pattern s; apply set_induction; clear s; intros.
+  trans_st (f x i).
+  apply fold_1; auto.
+  sym_st.
+  apply Comp; auto.
+  apply fold_1; auto.
+  trans_st (f x0 (fold f s (f x i))).
+  apply fold_2 with (eqA:=eqA); auto.
+  trans_st (f x0 (f x (fold f s i))).
+  trans_st (f x (f x0 (fold f s i))).
+  apply Comp; auto.
+  sym_st.
+  apply fold_2 with (eqA:=eqA); auto.
+  Qed.
+
+  Lemma fold_init : forall s, eqA i i' -> 
+   eqA (fold f s i) (fold f s i').
+  Proof. 
+  intros; pattern s; apply set_induction; clear s; intros.
+  trans_st i.
+  apply fold_1; auto.
+  trans_st i'.
+  sym_st; apply fold_1; auto.
+  trans_st (f x (fold f s i)).
+  apply fold_2 with (eqA:=eqA); auto.
+  trans_st (f x (fold f s i')).
+  sym_st; apply fold_2 with (eqA:=eqA); auto.
+  Qed.
+
+  End Fold_1.
+  Section Fold_2.
+  Variable i:A.
+
+  Lemma fold_union_inter : forall s s',
+   eqA (fold f (union s s') (fold f (inter s s') i))
+       (fold f s (fold f s' i)).
+  Proof.
+  intros; pattern s; apply set_induction; clear s; intros.
+  trans_st (fold f s' (fold f (inter s s') i)).
+  apply fold_equal; auto with set.
+  trans_st (fold f s' i).
+  apply fold_init; auto.
+  apply fold_1; auto with set.
+  sym_st; apply fold_1; auto.
+  rename s'0 into s''.
+  destruct (In_dec x s').
+  (* In x s' *)   
+  trans_st (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set.
+  apply fold_init; auto.
+  apply fold_2 with (eqA:=eqA); auto with set.
+  rewrite inter_iff; intuition.
+  trans_st (f x (fold f s (fold f s' i))).
+  trans_st (fold f (union s s') (f x (fold f (inter s s') i))).
+  apply fold_equal; auto.
+  apply equal_sym; apply union_Equal with x; auto with set.
+  trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
+  apply fold_commutes; auto.
+  sym_st; apply fold_2 with (eqA:=eqA); auto.
+  (* ~(In x s') *)
+  trans_st (f x (fold f (union s s') (fold f (inter s'' s') i))).
+  apply fold_2 with (eqA:=eqA); auto with set.
+  trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
+  apply Comp;auto.
+  apply fold_init;auto.
+  apply fold_equal;auto.
+  apply equal_sym; apply inter_Add_2 with x; auto with set.
+  trans_st (f x (fold f s (fold f s' i))).
+  sym_st; apply fold_2 with (eqA:=eqA); auto.
+  Qed.
+
+  End Fold_2.
+  Section Fold_3.
+  Variable i:A.
+
+  Lemma fold_diff_inter : forall s s', 
+   eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
+  Proof.
+  intros.
+  trans_st (fold f (union (diff s s') (inter s s')) 
+              (fold f (inter (diff s s') (inter s s')) i)).
+  sym_st; apply fold_union_inter; auto.
+  trans_st (fold f s (fold f (inter (diff s s') (inter s s')) i)).
+  apply fold_equal; auto with set.
+  apply fold_init; auto.
+  apply fold_1; auto with set.
+  Qed.
+
+  Lemma fold_union: forall s s', 
+   (forall x, ~(In x s/\In x s')) ->
+   eqA (fold f (union s s') i) (fold f s (fold f s' i)).
+  Proof.
+  intros.
+  trans_st (fold f (union s s') (fold f (inter s s') i)).
+  apply fold_init; auto.
+  sym_st; apply fold_1; auto with set.
+  unfold Empty; intro a; generalize (H a); set_iff; tauto.
+  apply fold_union_inter; auto.
+  Qed.
+
+  End Fold_3.
+  End Fold.
+
+  Lemma fold_plus :
+   forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
+  Proof.
+  assert (st := gen_st nat).
+  assert (fe : compat_op E.eq (@Logic.eq _) (fun _ => S)) by (unfold compat_op; auto). 
+  assert (fp : transpose (@Logic.eq _) (fun _:elt => S)) by (unfold transpose; auto).
+  intros s p; pattern s; apply set_induction; clear s; intros.
+  rewrite (fold_1 st p (fun _ => S) H).
+  rewrite (fold_1 st 0 (fun _ => S) H); trivial.
+  assert (forall p s', Add x s s' -> fold (fun _ => S) s' p = S (fold (fun _ => S) s p)).
+   change S with ((fun _ => S) x).  
+   intros; apply fold_2; auto.
+  rewrite H2; auto.
+  rewrite (H2 0); auto.
+  rewrite H.
+  simpl; auto.
+  Qed.
+
+  (** more properties of [cardinal] *)
+
+  Lemma empty_cardinal : cardinal empty = 0.
+  Proof.
+  rewrite cardinal_fold; apply fold_1; auto with set.
+  Qed.
+
+  Hint Immediate empty_cardinal cardinal_1 : set.
+
+  Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
+  Proof.
+  intros.
+  rewrite (singleton_equal_add x).
+  replace 0 with (cardinal empty); auto with set.
+  apply cardinal_2 with x; auto with set.
+  Qed.
+
+  Hint Resolve singleton_cardinal: set.
+
+  Lemma diff_inter_cardinal :
+   forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s .
+  Proof.
+  intros; do 3 rewrite cardinal_fold.
+  rewrite <- fold_plus.
+  apply fold_diff_inter with (eqA:=@Logic.eq nat); auto.
+  Qed.
+
+  Lemma union_cardinal: 
+   forall s s', (forall x, ~(In x s/\In x s')) -> 
+   cardinal (union s s')=cardinal s+cardinal s'.
+  Proof.
+  intros; do 3 rewrite cardinal_fold.
+  rewrite <- fold_plus.
+  apply fold_union; auto.
+  Qed.
+
+  Lemma subset_cardinal : 
+   forall s s', s[<=]s' -> cardinal s <= cardinal s' .
+  Proof.
+  intros.
+  rewrite <- (diff_inter_cardinal s' s).
+  rewrite (inter_sym s' s).
+  rewrite (inter_subset_equal H); auto with arith.
+  Qed.
+
+  Lemma subset_cardinal_lt : 
+   forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.
+  Proof. 
+  intros.
+  rewrite <- (diff_inter_cardinal s' s).
+  rewrite (inter_sym s' s).
+  rewrite (inter_subset_equal H).
+  generalize (@cardinal_inv_1 (diff s' s)).
+  destruct (cardinal (diff s' s)).
+  intro H2; destruct (H2 (refl_equal _) x).
+  set_iff; auto.
+  intros _.
+  change (0 + cardinal s < S n + cardinal s).
+  apply Plus.plus_lt_le_compat; auto with arith.
+  Qed. 
+
+  Theorem union_inter_cardinal :
+   forall s s', cardinal (union s s') + cardinal (inter s s')  = cardinal s  + cardinal s' .
+  Proof.
+  intros.
+  do 4 rewrite cardinal_fold.
+  do 2 rewrite <- fold_plus.
+  apply fold_union_inter with (eqA:=@Logic.eq nat); auto.
+  Qed.
+
+  Lemma union_cardinal_inter : 
+   forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
+  Proof.
+  intros.
+  rewrite <- union_inter_cardinal.
+  rewrite Plus.plus_comm.
+  auto with arith.
+  Qed.
+
+  Lemma union_cardinal_le : 
+   forall s s', cardinal (union s s') <= cardinal s  + cardinal s'.
+  Proof.
+   intros; generalize (union_inter_cardinal s s').
+   intros; rewrite <- H; auto with arith.
+  Qed.
+
+  Lemma add_cardinal_1 : 
+   forall s x, In x s -> cardinal (add x s) = cardinal s.
+  Proof.
+  auto with set.  
+  Qed.
+
+  Lemma add_cardinal_2 :
+   forall s x, ~In x s -> cardinal (add x s) = S (cardinal s).
+  Proof.
+  intros.
+  do 2 rewrite cardinal_fold.
+  change S with ((fun _ => S) x);
+   apply fold_add with (eqA:=@Logic.eq nat); auto.
+  Qed.
+
+  Lemma remove_cardinal_1 :
+   forall s x, In x s -> S (cardinal (remove x s)) = cardinal s.
+  Proof.
+  intros.
+  do 2 rewrite cardinal_fold.
+  change S with ((fun _ =>S) x).
+  apply remove_fold_1 with (eqA:=@Logic.eq nat); auto.
+  Qed.
+
+  Lemma remove_cardinal_2 : 
+   forall s x, ~In x s -> cardinal (remove x s) = cardinal s.
+  Proof. 
+  auto with set.
+  Qed.
+
+  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
+
+End WProperties.
+
+
+(** A clone of [WProperties] working on full sets. *)
 
 Module Properties (M:S).
   Module D := OT_as_DT M.E.
-  Include FSetWeakProperties.Properties M D.
+  Include WProperties D M.
 End Properties.
 
+
 (** Now comes some properties specific to the element ordering, 
-    invalid in FSetWeak. *)
+    invalid for Weak Sets. *)
 
 Module OrdProperties (M:S).
   Module ME:=OrderedTypeFacts(M.E).
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v
index de483f158..8c48bc24d 100644
--- a/theories/FSets/FSetToFiniteSet.v
+++ b/theories/FSets/FSetToFiniteSet.v
@@ -14,13 +14,13 @@
 (* $Id$ *)
 
 Require Import Ensembles Finite_sets.
-Require Import FSetInterface FSetProperties OrderedTypeEx.
+Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx.
 
 (** * Going from [FSets] with usual equality 
     to the old [Ensembles] and [Finite_sets] theory. *)
 
-Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U).
- Module MP:= Properties(M).
+Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
+ Module MP:= WProperties U M.
  Import M MP FM Ensembles Finite_sets.
 
  Definition mkEns : M.t -> Ensemble M.elt := 
@@ -82,7 +82,7 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U).
  Lemma add_Add : forall x s, !!(add x s) === Add _ (!!s) x.
  Proof.
  unfold Same_set, Included, mkEns, In.
- split; intro; set_iff; inversion 1; unfold E.eq; auto with sets.
+ split; intro; set_iff; inversion 1; auto with sets.
  inversion H0.
  constructor 2; constructor.
  constructor 1; auto.
@@ -97,7 +97,7 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U).
  inversion H0.
  constructor 2; constructor.
  constructor 1; auto.
- red in H; rewrite H; unfold E.eq in *.
+ red in H; rewrite H.
  inversion H0; auto.
  inversion H1; auto.
  Qed.
@@ -105,7 +105,7 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U).
  Lemma remove_Subtract : forall x s, !!(remove x s) === Subtract _ (!!s) x.
  Proof.
  unfold Same_set, Included, mkEns, In.
- split; intro; set_iff; inversion 1; unfold E.eq in *; auto with sets.
+ split; intro; set_iff; inversion 1; auto with sets.
  split; auto.
  contradict H1.
  inversion H1; auto.
@@ -136,4 +136,10 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U).
  apply Add_Add; auto.
  Qed.
 
+End WS_to_Finite_set.
+
+
+Module S_to_Finite_set (U:UsualOrderedType)(M: Sfun U).
+  Module D := OT_as_DT U.
+  Include WS_to_Finite_set D M.
 End S_to_Finite_set.
diff --git a/theories/FSets/FSetWeak.v b/theories/FSets/FSetWeak.v
deleted file mode 100644
index 080f2a4c2..000000000
--- a/theories/FSets/FSetWeak.v
+++ /dev/null
@@ -1,16 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Require Export DecidableType.
-Require Export DecidableTypeEx.
-Require Export FSetWeakInterface.
-Require Export FSetWeakFacts.
-Require Export FSetWeakProperties.
-Require Export FSetWeakList.
diff --git a/theories/FSets/FSetWeakEqProperties.v b/theories/FSets/FSetWeakEqProperties.v
deleted file mode 100644
index d5fa13bdd..000000000
--- a/theories/FSets/FSetWeakEqProperties.v
+++ /dev/null
@@ -1,934 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(** * Finite sets library *)
-
-(** This module proves many properties of finite sets that 
-    are consequences of the axiomatization in [FsetInterface] 
-    Contrary to the functor in [FsetWeakProperties] it uses 
-    sets operations instead of predicates over sets, i.e.
-    [mem x s=true] instead of [In x s], 
-    [equal s s'=true] instead of [Equal s s'], etc. *)
-
-Require Import FSetWeakProperties Zerob Sumbool Omega.
-
-Module EqProperties 
- (M:S)
- (D:DecidableType with Definition t:=M.E.t
-                  with Definition eq:=M.E.eq).
-Module Import MP := Properties M D.
-Import FM.
-Import M.E.
-Import M.
-
-Definition Add := MP.Add.
-
-Section BasicProperties. 
-
-(** Some old specifications written with boolean equalities. *) 
-
-Variable s s' s'': t.
-Variable x y z : elt.
-
-Lemma mem_eq: 
-  E.eq x y -> mem x s=mem y s.
-Proof. 
-intro H; rewrite H; auto.
-Qed.
-
-Lemma equal_mem_1: 
-  (forall a, mem a s=mem a s') -> equal s s'=true.
-Proof. 
-intros; apply equal_1; unfold Equal; intros.
-do 2 rewrite mem_iff; rewrite H; tauto.
-Qed.
-
-Lemma equal_mem_2: 
-  equal s s'=true -> forall a, mem a s=mem a s'.
-Proof. 
-intros; rewrite (equal_2 H); auto.
-Qed.
-
-Lemma subset_mem_1: 
-  (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
-Proof. 
-intros; apply subset_1; unfold Subset; intros a.
-do 2 rewrite mem_iff; auto.
-Qed.
-
-Lemma subset_mem_2: 
-  subset s s'=true -> forall a, mem a s=true -> mem a s'=true.
-Proof. 
-intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
-Qed.
-  
-Lemma empty_mem: mem x empty=false.
-Proof. 
-rewrite <- not_mem_iff; auto with set.
-Qed.
-
-Lemma is_empty_equal_empty: is_empty s = equal s empty.
-Proof. 
-apply bool_1; split; intros.
-rewrite <- (empty_is_empty_1 (s:=empty)); auto with set.
-rewrite <- is_empty_iff; auto with set.
-Qed.
-  
-Lemma choose_mem_1: choose s=Some x -> mem x s=true.
-Proof.  
-auto with set.
-Qed.
-
-Lemma choose_mem_2: choose s=None -> is_empty s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma add_mem_1: mem x (add x s)=true.
-Proof.
-auto with set.
-Qed.  
- 
-Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
-Proof. 
-apply add_neq_b.
-Qed.
-
-Lemma remove_mem_1: mem x (remove x s)=false.
-Proof. 
-rewrite <- not_mem_iff; auto with set.
-Qed. 
- 
-Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
-Proof. 
-apply remove_neq_b.
-Qed.
-
-Lemma singleton_equal_add: 
-  equal (singleton x) (add x empty)=true.
-Proof.
-rewrite (singleton_equal_add x); auto with set.
-Qed.  
-
-Lemma union_mem: 
-  mem x (union s s')=mem x s || mem x s'.
-Proof. 
-apply union_b.
-Qed.
-
-Lemma inter_mem: 
-  mem x (inter s s')=mem x s && mem x s'.
-Proof. 
-apply inter_b.
-Qed.
-
-Lemma diff_mem: 
-  mem x (diff s s')=mem x s && negb (mem x s').
-Proof. 
-apply diff_b.
-Qed.
-
-(** properties of [mem] *)
-
-Lemma mem_3 : ~In x s -> mem x s=false.
-Proof.
-intros; rewrite <- not_mem_iff; auto.
-Qed.
-
-Lemma mem_4 : mem x s=false -> ~In x s.
-Proof.
-intros; rewrite not_mem_iff; auto.
-Qed.
-
-(** Properties of [equal] *) 
-
-Lemma equal_refl: equal s s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma equal_sym: equal s s'=equal s' s.
-Proof.
-intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
-Qed.
-
-Lemma equal_trans: 
- equal s s'=true -> equal s' s''=true -> equal s s''=true.
-Proof.
-intros; rewrite (equal_2 H); auto.
-Qed.
-
-Lemma equal_equal: 
- equal s s'=true -> equal s s''=equal s' s''.
-Proof.
-intros; rewrite (equal_2 H); auto.
-Qed.
-
-Lemma equal_cardinal: 
- equal s s'=true -> cardinal s=cardinal s'.
-Proof.
-auto with set.
-Qed.
-
-(* Properties of [subset] *)
-
-Lemma subset_refl: subset s s=true. 
-Proof.
-auto with set.
-Qed.
-
-Lemma subset_antisym: 
- subset s s'=true -> subset s' s=true -> equal s s'=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma subset_trans: 
- subset s s'=true -> subset s' s''=true -> subset s s''=true.
-Proof.
-do 3 rewrite <- subset_iff; intros.
-apply subset_trans with s'; auto.
-Qed.
-
-Lemma subset_equal: 
- equal s s'=true -> subset s s'=true.
-Proof.
-auto with set.
-Qed.
-
-(** Properties of [choose] *)
-
-Lemma choose_mem_3: 
- is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
-Proof.
-intros.
-generalize (@choose_1 s) (@choose_2 s).
-destruct (choose s);intros.
-exists e;auto with set.
-generalize (H1 (refl_equal None)); clear H1.
-intros; rewrite (is_empty_1 H1) in H; discriminate.
-Qed.
-
-Lemma choose_mem_4: choose empty=None.
-Proof.
-generalize (@choose_1 empty).
-case (@choose empty);intros;auto.
-elim (@empty_1 e); auto.
-Qed.
-
-(** Properties of [add] *)
-
-Lemma add_mem_3: 
- mem y s=true -> mem y (add x s)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma add_equal: 
- mem x s=true -> equal (add x s) s=true.
-Proof.
-auto with set.
-Qed.
-
-(** Properties of [remove] *)
-
-Lemma remove_mem_3: 
- mem y (remove x s)=true -> mem y s=true.
-Proof.
-rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
-Qed.
-
-Lemma remove_equal: 
- mem x s=false -> equal (remove x s) s=true.
-Proof.
-intros; apply equal_1; apply remove_equal.
-rewrite not_mem_iff; auto.
-Qed.
-
-Lemma add_remove: 
- mem x s=true -> equal (add x (remove x s)) s=true.
-Proof.
-intros; apply equal_1; apply add_remove; auto with set.
-Qed.
-
-Lemma remove_add: 
- mem x s=false -> equal (remove x (add x s)) s=true.
-Proof.
-intros; apply equal_1; apply remove_add; auto.
-rewrite not_mem_iff; auto.
-Qed.
-
-(** Properties of [is_empty] *)
-
-Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
-Proof.
-intros; apply bool_1; split; intros.
-rewrite MP.cardinal_1; simpl; auto with set.
-assert (cardinal s = 0) by (apply zerob_true_elim; auto).
-auto with set.
-Qed.
-
-(** Properties of [singleton] *)
-
-Lemma singleton_mem_1: mem x (singleton x)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
-Proof.
-intros; rewrite singleton_b.
-unfold eqb; destruct (eq_dec x y); intuition.
-Qed.
-
-Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
-Proof.
-intros; apply singleton_1; auto with set.
-Qed.
-
-(** Properties of [union] *)
-
-Lemma union_sym:
- equal (union s s') (union s' s)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_subset_equal: 
- subset s s'=true -> equal (union s s') s'=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_equal_1: 
- equal s s'=true-> equal (union s s'') (union s' s'')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_equal_2: 
- equal s' s''=true-> equal (union s s') (union s s'')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_assoc: 
- equal (union (union s s') s'') (union s (union s' s''))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma add_union_singleton: 
- equal (add x s) (union (singleton x) s)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_add: 
- equal (union (add x s) s') (add x (union s s'))=true.
-Proof.
-auto with set.
-Qed.
-
-(* caracterisation of [union] via [subset] *)
-
-Lemma union_subset_1: subset s (union s s')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_subset_2: subset s' (union s s')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_subset_3:
- subset s s''=true -> subset s' s''=true -> 
-  subset (union s s') s''=true.
-Proof.
-intros; apply subset_1; apply union_subset_3; auto with set.
-Qed.
-
-(** Properties of [inter] *) 
-
-Lemma inter_sym: equal (inter s s') (inter s' s)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_subset_equal: 
- subset s s'=true -> equal (inter s s') s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_equal_1: 
- equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_equal_2: 
- equal s' s''=true -> equal (inter s s') (inter s s'')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_assoc: 
- equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_inter_1: 
- equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_inter_2: 
- equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_add_1: mem x s'=true -> 
- equal (inter (add x s) s') (add x (inter s s'))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_add_2: mem x s'=false -> 
- equal (inter (add x s) s') (inter s s')=true.
-Proof.
-intros; apply equal_1; apply inter_add_2.
-rewrite not_mem_iff; auto.
-Qed.
-
-(* caracterisation of [union] via [subset] *)
-
-Lemma inter_subset_1: subset (inter s s') s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_subset_2: subset (inter s s') s'=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_subset_3:
- subset s'' s=true -> subset s'' s'=true -> 
-  subset s'' (inter s s')=true.
-Proof.
-intros; apply subset_1; apply inter_subset_3; auto with set.
-Qed.
-
-(** Properties of [diff] *)
-
-Lemma diff_subset: subset (diff s s') s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma diff_subset_equal:
- subset s s'=true -> equal (diff s s') empty=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma remove_inter_singleton: 
- equal (remove x s) (diff s (singleton x))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma diff_inter_empty:
- equal (inter (diff s s') (inter s s')) empty=true. 
-Proof.
-auto with set.
-Qed.
-
-Lemma diff_inter_all: 
- equal (union (diff s s') (inter s s')) s=true.
-Proof.
-auto with set.
-Qed.
-
-End BasicProperties.
-
-Hint Immediate empty_mem is_empty_equal_empty add_mem_1
-   remove_mem_1 singleton_equal_add union_mem inter_mem
-   diff_mem equal_sym add_remove remove_add : set. 
-Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
-   choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
-   subset_refl subset_equal subset_antisym
-   add_mem_3 add_equal remove_mem_3 remove_equal : set.
-
-
-(** General recursion principle *)
-
-Lemma set_rec:  forall (P:t->Type),
- (forall s s', equal s s'=true -> P s -> P s') -> 
- (forall s x, mem x s=false -> P s -> P (add x s)) -> 
- P empty -> forall s, P s.
-Proof.
-intros.
-apply set_induction; auto; intros.
-apply X with empty; auto with set.
-apply X with (add x s0); auto with set.
-apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto.
-apply X0; auto with set; apply mem_3; auto.
-Qed.
-
-(** Properties of [fold] *)
-
-Lemma exclusive_set : forall s s' x,
- ~(In x s/\In x s') <-> mem x s && mem x s'=false.
-Proof.
-intros; do 2 rewrite mem_iff.
-destruct (mem x s); destruct (mem x s'); intuition.
-Qed.
-
-Section Fold. 
-Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
-Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
-Variables (i:A).
-Variables (s s':t)(x:elt).
- 
-Lemma fold_empty: (fold f empty i) = i.
-Proof. 
-apply fold_empty; auto.
-Qed.
-
-Lemma fold_equal: 
- equal s s'=true -> eqA (fold f s i) (fold f s' i).
-Proof. 
-intros; apply fold_equal with (eqA:=eqA); auto with set.
-Qed.
-   
-Lemma fold_add: 
- mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
-Proof. 
-intros; apply fold_add with (eqA:=eqA); auto.
-rewrite not_mem_iff; auto.
-Qed.
-
-Lemma add_fold: 
-  mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
-Proof.
-intros; apply add_fold with (eqA:=eqA); auto with set.
-Qed.
-
-Lemma remove_fold_1: 
- mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
-Proof.
-intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
-Qed.
-
-Lemma remove_fold_2: 
- mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
-Proof.
-intros; apply remove_fold_2 with (eqA:=eqA); auto.
-rewrite not_mem_iff; auto.
-Qed.
-
-Lemma fold_union: 
- (forall x, mem x s && mem x s'=false) -> 
- eqA (fold f (union s s') i) (fold f s (fold f s' i)).
-Proof.
-intros; apply fold_union with (eqA:=eqA); auto.
-intros; rewrite exclusive_set; auto.
-Qed.
-
-End Fold.
-
-(** Properties of [cardinal] *)
-
-Lemma add_cardinal_1: 
- forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
-Proof.
-auto with set.
-Qed.
-
-Lemma add_cardinal_2: 
- forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
-Proof.
-intros; apply add_cardinal_2; auto.
-rewrite not_mem_iff; auto.
-Qed.
-
-Lemma remove_cardinal_1: 
- forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
-Proof.
-intros; apply remove_cardinal_1; auto with set.
-Qed.
-
-Lemma remove_cardinal_2: 
- forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
-Proof.
-intros; apply Equal_cardinal; apply equal_2; auto with set.
-Qed.
-
-Lemma union_cardinal: 
- forall s s', (forall x, mem x s && mem x s'=false) -> 
- cardinal (union s s')=cardinal s+cardinal s'.
-Proof.
-intros; apply union_cardinal; auto; intros.
-rewrite exclusive_set; auto.
-Qed.
-
-Lemma subset_cardinal: 
- forall s s', subset s s'=true -> cardinal s<=cardinal s'.
-Proof.
-intros; apply subset_cardinal; auto with set.
-Qed.
-
-Section Bool.
-
-(** Properties of [filter] *)
-
-Variable f:elt->bool.
-Variable Comp: compat_bool E.eq f.
-
-Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
-Proof.
-unfold compat_bool in *; intros; f_equal; auto.
-Qed.
-
-Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
-Proof. 
-intros; apply filter_b; auto.
-Qed.
-
-Lemma for_all_filter: 
- forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
-Proof. 
-intros; apply bool_1; split; intros.
-apply is_empty_1.
-unfold Empty; intros. 
-rewrite filter_iff; auto.
-red; destruct 1.
-rewrite <- (@for_all_iff s f) in H; auto.
-rewrite (H a H0) in H1; discriminate.
-apply for_all_1; auto; red; intros.
-revert H; rewrite <- is_empty_iff.
-unfold Empty; intro H; generalize (H x); clear H.
-rewrite filter_iff; auto.
-destruct (f x); auto.
-Qed.
-
-Lemma exists_filter : 
- forall s, exists_ f s=negb (is_empty (filter f s)).
-Proof. 
-intros; apply bool_1; split; intros. 
-destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).
-apply bool_6.
-red; intros; apply (@is_empty_2 _ H0 a); auto with set.
-generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)).
-destruct (choose (filter f s)).
-intros H0 _; apply exists_1; auto.
-exists e; generalize (H0 e); rewrite filter_iff; auto.
-intros _ H0.
-rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate.
-Qed.
-
-Lemma partition_filter_1: 
- forall s, equal (fst (partition f s)) (filter f s)=true.
-Proof. 
-auto with set.
-Qed.
-
-Lemma partition_filter_2: 
- forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
-Proof. 
-auto with set.
-Qed.
-
-Lemma filter_add_1 : forall s x, f x = true -> 
- filter f (add x s) [=] add x (filter f s). 
-Proof.
-red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
-intuition.
-rewrite <- H; apply Comp; auto.
-Qed.
-
-Lemma filter_add_2 : forall s x, f x = false -> 
- filter f (add x s) [=] filter f s. 
-Proof.
-red; intros; do 2 (rewrite filter_iff; auto); set_iff.
-intuition.
-assert (f x = f a) by (apply Comp; auto).
-rewrite H in H1; rewrite H2 in H1; discriminate.
-Qed.
-
-Lemma add_filter_1 : forall s s' x, 
- f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
-Proof.
-unfold Add, MP.Add; intros.
-repeat rewrite filter_iff; auto.
-rewrite H0; clear H0.
-assert (E.eq x y -> f y = true) by 
- (intro H0; rewrite <- (Comp _ _ H0); auto).
-tauto.
-Qed.
-
-Lemma add_filter_2 : forall s s' x, 
- f x=false -> (Add x s s') -> filter f s [=] filter f s'.
-Proof.
-unfold Add, MP.Add, Equal; intros.
-repeat rewrite filter_iff; auto.
-rewrite H0; clear H0.
-assert (f a = true -> ~E.eq x a).
- intros H0 H1.
- rewrite (Comp _ _ H1) in H.
- rewrite H in H0; discriminate.
-tauto. 
-Qed.
-
-Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
-  forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
-Proof.
-clear Comp' Comp f.
-intros.
-assert (compat_bool E.eq (fun x => orb (f x) (g x))).
-  unfold compat_bool; intros.
-  rewrite (H x y H1);  rewrite (H0 x y H1); auto.
-unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto.
-assert (f a || g a = true <-> f a = true \/ g a = true).
-  split; auto with bool.
-  intro H3; destruct (orb_prop _ _ H3); auto.
-tauto.
-Qed.
-
-Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').
-Proof.
-unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.
-Qed.
-
-(** Properties of [for_all] *)
-
-Lemma for_all_mem_1: forall s, 
- (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
-Proof.
-intros.
-rewrite for_all_filter; auto.
-rewrite is_empty_equal_empty.
-apply equal_mem_1;intros.
-rewrite filter_b; auto.
-rewrite empty_mem.
-generalize (H a); case (mem a s);intros;auto.
-rewrite H0;auto.
-Qed.
-
-Lemma for_all_mem_2: forall s, 
- (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true. 
-Proof.
-intros.
-rewrite for_all_filter in H; auto.
-rewrite is_empty_equal_empty in H.
-generalize (equal_mem_2 _ _ H x).
-rewrite filter_b; auto.
-rewrite empty_mem.
-rewrite H0; simpl;intros.
-replace true with (negb false);auto;apply negb_sym;auto.
-Qed.
-
-Lemma for_all_mem_3: 
- forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
-Proof.
-intros.
-apply (bool_eq_ind (for_all f s));intros;auto.
-rewrite for_all_filter in H1; auto.
-rewrite is_empty_equal_empty in H1.
-generalize (equal_mem_2 _ _ H1 x).
-rewrite filter_b; auto.
-rewrite empty_mem.
-rewrite H.
-rewrite H0.
-simpl;auto.
-Qed.
-
-Lemma for_all_mem_4: 
- forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
-Proof.
-intros.
-rewrite for_all_filter in H; auto.
-destruct (choose_mem_3 _ H) as (x,(H0,H1));intros.
-exists x.
-rewrite filter_b in H1; auto.
-elim (andb_prop _ _ H1).
-split;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
-Qed.
-
-(** Properties of [exists] *)
-
-Lemma for_all_exists: 
- forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
-Proof.
-intros.
-rewrite for_all_b; auto.
-rewrite exists_b; auto.
-induction (elements s); simpl; auto.
-destruct (f a); simpl; auto.
-Qed.
-
-End Bool.
-Section Bool'.
-
-Variable f:elt->bool.
-Variable Comp: compat_bool E.eq f.
-
-Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
-Proof.
-unfold compat_bool in *; intros; f_equal; auto.
-Qed.
-
-Lemma exists_mem_1: 
- forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
-Proof.
-intros.
-rewrite for_all_exists; auto.
-rewrite for_all_mem_1;auto with bool.
-intros;generalize (H x H0);intros. 
-symmetry;apply negb_sym;simpl;auto.
-Qed.
-
-Lemma exists_mem_2: 
- forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false. 
-Proof.
-intros.
-rewrite for_all_exists in H; auto.
-replace false with (negb true);auto;apply negb_sym;symmetry.
-rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
-Qed.
-
-Lemma exists_mem_3: 
- forall s x, mem x s=true -> f x=true -> exists_ f s=true.
-Proof.
-intros.
-rewrite for_all_exists; auto.
-symmetry;apply negb_sym;simpl.
-apply for_all_mem_3 with x;auto.
-rewrite H0;auto.
-Qed.
-
-Lemma exists_mem_4: 
- forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
-Proof.
-intros.
-rewrite for_all_exists in H; auto.
-elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros.
-elim p;intros.
-exists x;split;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
-Qed.
-
-End Bool'.
-
-Section Sum.
-
-(** Adding a valuation function on all elements of a set. *)
-
-Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. 
-Notation compat_opL := (compat_op E.eq (@Logic.eq _)).
-Notation transposeL := (transpose (@Logic.eq _)).
-
-Lemma sum_plus : 
-  forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
-    forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
-Proof.
-unfold sum.
-intros f g Hf Hg.
-assert (fc : compat_opL (fun x:elt =>plus (f x))).  auto.
-assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
-assert (gc : compat_opL (fun x:elt => plus (g x))). auto.
-assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
-assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto.
-assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
-assert (st := gen_st nat).
-intros s;pattern s; apply set_rec.
-intros.
-rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
-rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H).
-rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto.
-intros; do 3 (rewrite (fold_add _ _ st);auto).
-rewrite H0;simpl;omega.
-do 3 rewrite fold_empty;auto.
-Qed.
-
-Lemma sum_filter : forall f, (compat_bool E.eq f) -> 
-  forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
-Proof.
-unfold sum; intros f Hf.
-assert (st := gen_st nat).
-assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))). 
- red; intros.
- rewrite (Hf x x' H); auto.
-assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
- red; intros; omega.
-intros s;pattern s; apply set_rec.
-intros.
-change elt with E.t.
-rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H).
-rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto.
-intros; rewrite (fold_add _ _ st _ cc ct); auto.
-generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) .
-assert (~ In x (filter f s0)).
- intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H.
-case (f x); simpl; intros.
-rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto.
-rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto.
-intros; rewrite fold_empty;auto.
-rewrite MP.cardinal_1; auto.
-unfold Empty; intros.
-rewrite filter_iff; auto; set_iff; tauto.
-Qed.
-
-Lemma fold_compat : 
-  forall (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA))
-  (f g:elt->A->A),
-  (compat_op E.eq eqA f) -> (transpose eqA f) -> 
-  (compat_op E.eq eqA g) -> (transpose eqA g) -> 
-  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> 
-  (eqA (fold f s i) (fold g s i)).
-Proof.
-intros A eqA st f g fc ft gc gt i.
-intro s; pattern s; apply set_rec; intros.
-trans_st (fold f s0 i).
-apply fold_equal with (eqA:=eqA); auto.
-rewrite equal_sym; auto.
-trans_st (fold g s0 i).
-apply H0; intros; apply H1; auto with set.
-elim  (equal_2 H x); auto with set; intros.
-apply fold_equal with (eqA:=eqA); auto with set.
-trans_st (f x (fold f s0 i)).
-apply fold_add with (eqA:=eqA); auto with set.
-trans_st (g x (fold f s0 i)); auto with set.
-trans_st (g x (fold g s0 i)); auto with set.
-sym_st; apply fold_add with (eqA:=eqA); auto.
-do 2 rewrite fold_empty; refl_st.
-Qed.
-
-Lemma sum_compat : 
-  forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
-  forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
-intros.
-unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto.
-red; intros; omega.
-red; intros; omega.
-Qed.
-
-End Sum.
-
-End EqProperties. 
diff --git a/theories/FSets/FSetWeakFacts.v b/theories/FSets/FSetWeakFacts.v
deleted file mode 100644
index 0740d7f8e..000000000
--- a/theories/FSets/FSetWeakFacts.v
+++ /dev/null
@@ -1,494 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(** * Finite sets library *)
-
-(** This functor derives additional facts from [FSetInterface.S]. These
-  facts are mainly the specifications of [FSetInterface.S] written using 
-  different styles: equivalence and boolean equalities. 
-  Moreover, we prove that [E.Eq] and [Equal] are setoid equalities.
-*)
-
-Require Import DecidableTypeEx.
-Require Export FSetWeakInterface. 
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-Module Facts 
- (M:FSetWeakInterface.S)
- (D:DecidableType with Definition t:=M.E.t with Definition eq:=M.E.eq).
-Import M.E.
-Import M.
-
-Notation eq_dec := D.eq_dec.
-Definition eqb x y := if eq_dec x y then true else false.
-
-(** * Specifications written using equivalences *)
-
-Section IffSpec. 
-Variable s s' s'' : t.
-Variable x y z : elt.
-
-Lemma In_eq_iff : E.eq x y -> (In x s <-> In y s).
-Proof.
-split; apply In_1; auto.
-Qed.
-
-Lemma mem_iff : In x s <-> mem x s = true.
-Proof.
-split; [apply mem_1|apply mem_2].
-Qed.
-
-Lemma not_mem_iff : ~In x s <-> mem x s = false.
-Proof.
-rewrite mem_iff; destruct (mem x s); intuition.
-Qed.
-
-Lemma equal_iff : s[=]s' <-> equal s s' = true.
-Proof. 
-split; [apply equal_1|apply equal_2].
-Qed.
-
-Lemma subset_iff : s[<=]s' <-> subset s s' = true.
-Proof. 
-split; [apply subset_1|apply subset_2].
-Qed.
-
-Lemma empty_iff : In x empty <-> False.
-Proof.
-intuition; apply (empty_1 H).
-Qed.
-
-Lemma is_empty_iff : Empty s <-> is_empty s = true. 
-Proof. 
-split; [apply is_empty_1|apply is_empty_2].
-Qed.
-
-Lemma singleton_iff : In y (singleton x) <-> E.eq x y.
-Proof.
-split; [apply singleton_1|apply singleton_2].
-Qed.
-
-Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s.
-Proof. 
-split; [ | destruct 1; [apply add_1|apply add_2]]; auto.
-destruct (eq_dec x y) as [E|E]; auto.
-intro H; right; exact (add_3 E H).
-Qed.
-
-Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s)  <-> In y s).
-Proof.
-split; [apply add_3|apply add_2]; auto.
-Qed.
-
-Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y.
-Proof.
-split; [split; [apply remove_3 with x |] | destruct 1; apply remove_2]; auto.
-intro.
-apply (remove_1 H0 H).
-Qed.
-
-Lemma remove_neq_iff : ~ E.eq x y -> (In y (remove x s) <-> In y s).
-Proof.
-split; [apply remove_3|apply remove_2]; auto.
-Qed.
-
-Lemma union_iff : In x (union s s') <-> In x s \/ In x s'.
-Proof.
-split; [apply union_1 | destruct 1; [apply union_2|apply union_3]]; auto.
-Qed.
-
-Lemma inter_iff : In x (inter s s') <-> In x s /\ In x s'.
-Proof.
-split; [split; [apply inter_1 with s' | apply inter_2 with s] | destruct 1; apply inter_3]; auto.
-Qed.
-
-Lemma diff_iff : In x (diff s s') <-> In x s /\ ~ In x s'.
-Proof.
-split; [split; [apply diff_1 with s' | apply diff_2 with s] | destruct 1; apply diff_3]; auto.
-Qed.
-
-Variable f : elt->bool.
-
-Lemma filter_iff :  compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true).
-Proof. 
-split; [split; [apply filter_1 with f | apply filter_2 with s] | destruct 1; apply filter_3]; auto. 
-Qed.
-
-Lemma for_all_iff : compat_bool E.eq f ->
-  (For_all (fun x => f x = true) s <-> for_all f s = true).
-Proof.
-split; [apply for_all_1 | apply for_all_2]; auto.
-Qed.
- 
-Lemma exists_iff : compat_bool E.eq f ->
-  (Exists (fun x => f x = true) s <-> exists_ f s = true).
-Proof.
-split; [apply exists_1 | apply exists_2]; auto.
-Qed.
-
-Lemma elements_iff : In x s <-> InA E.eq x (elements s).
-Proof. 
-split; [apply elements_1 | apply elements_2].
-Qed.
-
-End IffSpec.
-
-(** Useful tactic for simplifying expressions like [In y (add x (union s s'))] *)
-  
-Ltac set_iff := 
- repeat (progress (
-  rewrite add_iff || rewrite remove_iff || rewrite singleton_iff 
-  || rewrite union_iff || rewrite inter_iff || rewrite diff_iff
-  || rewrite empty_iff)).
-
-(**  * Specifications written using boolean predicates *)
-
-Section BoolSpec.
-Variable s s' s'' : t.
-Variable x y z : elt.
-
-Lemma mem_b : E.eq x y -> mem x s = mem y s.
-Proof. 
-intros.
-generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H).
-destruct (mem x s); destruct (mem y s); intuition.
-Qed.
-
-Lemma empty_b : mem y empty = false.
-Proof.
-generalize (empty_iff y)(mem_iff empty y).
-destruct (mem y empty); intuition.
-Qed.
-
-Lemma add_b : mem y (add x s) = eqb x y || mem y s.
-Proof.
-generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb.
-destruct (eq_dec x y); destruct (mem y s); destruct (mem y (add x s)); intuition.
-Qed.
-
-Lemma add_neq_b : ~ E.eq x y -> mem y (add x s) = mem y s.
-Proof.
-intros; generalize (mem_iff (add x s) y)(mem_iff s y)(add_neq_iff s H).
-destruct (mem y s); destruct (mem y (add x s)); intuition.
-Qed.
-
-Lemma remove_b : mem y (remove x s) = mem y s && negb (eqb x y).
-Proof.
-generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_iff s x y); unfold eqb.
-destruct (eq_dec x y); destruct (mem y s); destruct (mem y (remove x s)); simpl; intuition.
-Qed.
-
-Lemma remove_neq_b : ~ E.eq x y -> mem y (remove x s) = mem y s.
-Proof.
-intros; generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_neq_iff s H).
-destruct (mem y s); destruct (mem y (remove x s)); intuition.
-Qed.
-
-Lemma singleton_b : mem y (singleton x) = eqb x y.
-Proof. 
-generalize (mem_iff (singleton x) y)(singleton_iff x y); unfold eqb.
-destruct (eq_dec x y); destruct (mem y (singleton x)); intuition.
-Qed.
-
-Lemma union_b : mem x (union s s') = mem x s || mem x s'.
-Proof.
-generalize (mem_iff (union s s') x)(mem_iff s x)(mem_iff s' x)(union_iff s s' x).
-destruct (mem x s); destruct (mem x s'); destruct (mem x (union s s')); intuition.
-Qed.
-
-Lemma inter_b : mem x (inter s s') = mem x s && mem x s'.
-Proof.
-generalize (mem_iff (inter s s') x)(mem_iff s x)(mem_iff s' x)(inter_iff s s' x).
-destruct (mem x s); destruct (mem x s'); destruct (mem x (inter s s')); intuition.
-Qed.
-
-Lemma diff_b : mem x (diff s s') = mem x s && negb (mem x s').
-Proof.
-generalize (mem_iff (diff s s') x)(mem_iff s x)(mem_iff s' x)(diff_iff s s' x).
-destruct (mem x s); destruct (mem x s'); destruct (mem x (diff s s')); simpl; intuition.
-Qed.
-
-Lemma elements_b : mem x s = existsb (eqb x) (elements s).
-Proof.
-generalize (mem_iff s x)(elements_iff s x)(existsb_exists (eqb x) (elements s)).
-rewrite InA_alt.
-destruct (mem x s); destruct (existsb (eqb x) (elements s)); auto; intros.
-symmetry.
-rewrite H1.
-destruct H0 as (H0,_).
-destruct H0 as (a,(Ha1,Ha2)); [ intuition |].
-exists a; intuition.
-unfold eqb; destruct (eq_dec x a); auto.
-rewrite <- H.
-rewrite H0.
-destruct H1 as (H1,_).
-destruct H1 as (a,(Ha1,Ha2)); [intuition|].
-exists a; intuition.
-unfold eqb in *; destruct (eq_dec x a); auto; discriminate.
-Qed.
-
-Variable f : elt->bool.
-
-Lemma filter_b : compat_bool E.eq f -> mem x (filter f s) = mem x s && f x.
-Proof. 
-intros.
-generalize (mem_iff (filter f s) x)(mem_iff s x)(filter_iff s x H).
-destruct (mem x s); destruct (mem x (filter f s)); destruct (f x); simpl; intuition.
-Qed.
-
-Lemma for_all_b : compat_bool E.eq f ->
-  for_all f s = forallb f (elements s).
-Proof.
-intros.
-generalize (forallb_forall f (elements s))(for_all_iff s H)(elements_iff s).
-unfold For_all.
-destruct (forallb f (elements s)); destruct (for_all f s); auto; intros.
-rewrite <- H1; intros.
-destruct H0 as (H0,_).
-rewrite (H2 x0) in H3.
-rewrite (InA_alt E.eq x0 (elements s)) in H3.
-destruct H3 as (a,(Ha1,Ha2)).
-rewrite (H _ _ Ha1).
-apply H0; auto.
-symmetry.
-rewrite H0; intros.
-destruct H1 as (_,H1).
-apply H1; auto.
-rewrite H2.
-rewrite InA_alt; eauto.
-Qed.
-
-Lemma exists_b : compat_bool E.eq f -> 
-  exists_ f s = existsb f (elements s).
-Proof.
-intros.
-generalize (existsb_exists f (elements s))(exists_iff s H)(elements_iff s).
-unfold Exists.
-destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros.
-rewrite <- H1; intros.
-destruct H0 as (H0,_).
-destruct H0 as (a,(Ha1,Ha2)); auto.
-exists a; split; auto.
-rewrite H2; rewrite InA_alt; eauto.
-symmetry.
-rewrite H0.
-destruct H1 as (_,H1).
-destruct H1 as (a,(Ha1,Ha2)); auto.
-rewrite (H2 a) in Ha1.
-rewrite (InA_alt E.eq a (elements s)) in Ha1.
-destruct Ha1 as (b,(Hb1,Hb2)).
-exists b; auto.
-rewrite <- (H _ _ Hb1); auto.
-Qed.
-
-End BoolSpec.
-
-(** * [E.eq] and [Equal] are setoid equalities *)
-
-Definition E_ST : Setoid_Theory elt E.eq.
-Proof.
-constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
-Qed.
-
-Definition Equal_ST : Setoid_Theory t Equal.
-Proof. 
-constructor; [apply eq_refl | apply eq_sym | apply eq_trans].
-Qed.
-
-Add Relation elt E.eq 
- reflexivity proved by E.eq_refl 
- symmetry proved by E.eq_sym
- transitivity proved by E.eq_trans 
- as EltSetoid.
-
-Add Relation t Equal 
- reflexivity proved by eq_refl 
- symmetry proved by eq_sym
- transitivity proved by eq_trans 
- as EqualSetoid.
-
-Add Morphism In with signature E.eq ==> Equal ==> iff as In_m.
-Proof.
-unfold Equal; intros x y H s s' H0.
-rewrite (In_eq_iff s H); auto.
-Qed.
-
-Add Morphism is_empty : is_empty_m.
-Proof.
-unfold Equal; intros s s' H.
-generalize (is_empty_iff s)(is_empty_iff s').
-destruct (is_empty s); destruct (is_empty s'); 
- unfold Empty; auto; intros.
-symmetry.
-rewrite <- H1; intros a Ha.
-rewrite <- (H a) in Ha.
-destruct H0 as (_,H0).
-exact (H0 (refl_equal true) _ Ha).
-rewrite <- H0; intros a Ha.
-rewrite (H a) in Ha.
-destruct H1 as (_,H1).
-exact (H1 (refl_equal true) _ Ha).
-Qed.
-
-Add Morphism Empty with signature Equal ==> iff as Empty_m.
-Proof. 
-intros; do 2 rewrite is_empty_iff; rewrite H; intuition.
-Qed.
-
-Add Morphism mem : mem_m.
-Proof.
-unfold Equal; intros x y H s s' H0.
-generalize (H0 x); clear H0; rewrite (In_eq_iff s' H).
-generalize (mem_iff s x)(mem_iff s' y).
-destruct (mem x s); destruct (mem y s'); intuition.
-Qed.
-
-Add Morphism singleton : singleton_m.
-Proof.
-unfold Equal; intros x y H a.
-do 2 rewrite singleton_iff; split; intros.
-apply E.eq_trans with x; auto.
-apply E.eq_trans with y; auto.
-Qed.
-
-Add Morphism add : add_m.
-Proof.
-unfold Equal; intros x y H s s' H0 a.
-do 2 rewrite add_iff; rewrite H; rewrite H0; intuition.
-Qed.
-
-Add Morphism remove : remove_m.
-Proof.
-unfold Equal; intros x y H s s' H0 a.
-do 2 rewrite remove_iff; rewrite H; rewrite H0; intuition.
-Qed.
-
-Add Morphism union : union_m.
-Proof.
-unfold Equal; intros s s' H s'' s''' H0 a.
-do 2 rewrite union_iff; rewrite H; rewrite H0; intuition.
-Qed.
-
-Add Morphism inter : inter_m.
-Proof.
-unfold Equal; intros s s' H s'' s''' H0 a.
-do 2 rewrite inter_iff; rewrite H; rewrite H0; intuition.
-Qed.
-
-Add Morphism diff : diff_m.
-Proof.
-unfold Equal; intros s s' H s'' s''' H0 a.
-do 2 rewrite diff_iff; rewrite H; rewrite H0; intuition.
-Qed.
-
-Add Morphism Subset with signature Equal ==> Equal ==> iff as  Subset_m.
-Proof. 
-unfold Equal, Subset; firstorder.
-Qed.
-
-Add Morphism subset : subset_m.
-Proof.
-intros s s' H s'' s''' H0.
-generalize (subset_iff s s'') (subset_iff s' s'''). 
-destruct (subset s s''); destruct (subset s' s'''); auto; intros.
-rewrite H in H1; rewrite H0 in H1; intuition.
-rewrite H in H1; rewrite H0 in H1; intuition.
-Qed.
-
-Add Morphism equal : equal_m.
-Proof.
-intros s s' H s'' s''' H0.
-generalize (equal_iff s s'') (equal_iff s' s''').
-destruct (equal s s''); destruct (equal s' s'''); auto; intros.
-rewrite H in H1; rewrite H0 in H1; intuition.
-rewrite H in H1; rewrite H0 in H1; intuition.
-Qed.
-
-
-(* [Subset] is a setoid order *)
-
-Lemma Subset_refl : forall s, s[<=]s.
-Proof. red; auto. Defined.
-
-Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''.
-Proof. unfold Subset; eauto. Defined.
-
-Add Relation t Subset 
- reflexivity proved by Subset_refl
- transitivity proved by Subset_trans
- as SubsetSetoid.
-(* NB: for the moment, it is important to use Defined and not Qed in 
-   the two previous lemmas, in order to allow conversion of 
-   SubsetSetoid coming from separate Facts modules. See bug #1738. *)
-
-Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m.
-Proof.
-unfold Subset, impl; intros; eauto with set.
-Qed.
-
-Add Morphism Empty with signature Subset --> impl as Empty_s_m.
-Proof. 
-unfold Subset, Empty, impl; firstorder.
-Qed.
-
-Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m.
-Proof.
-unfold Subset; intros x y H s s' H0 a.
-do 2 rewrite add_iff; rewrite H; intuition.
-Qed.
-
-Add Morphism remove with signature E.eq ==> Subset ++> Subset as remove_s_m.
-Proof.
-unfold Subset; intros x y H s s' H0 a.
-do 2 rewrite remove_iff; rewrite H; intuition.
-Qed.
-
-Add Morphism union with signature Subset ++> Subset ++> Subset as union_s_m.
-Proof.
-unfold Equal; intros s s' H s'' s''' H0 a.
-do 2 rewrite union_iff; intuition.
-Qed.
-
-Add Morphism inter with signature Subset ++> Subset ++> Subset as inter_s_m.
-Proof.
-unfold Equal; intros s s' H s'' s''' H0 a.
-do 2 rewrite inter_iff; intuition.
-Qed.
-
-Add Morphism diff with signature Subset ++> Subset --> Subset as diff_s_m.
-Proof.
-unfold Subset; intros s s' H s'' s''' H0 a.
-do 2 rewrite diff_iff; intuition.
-Qed.
-
-(* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism
-   without additional hypothesis on [f]. For instance: *)
-
-Lemma filter_equal : forall f, compat_bool E.eq f -> 
-  forall s s', s[=]s' -> filter f s [=] filter f s'.
-Proof.
-unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto.
-Qed.
-
-Lemma filter_subset : forall f, compat_bool E.eq f -> 
-  forall s s', s[<=]s' -> filter f s [<=] filter f s'.
-Proof.
-unfold Subset; intros; rewrite filter_iff in *; intuition.
-Qed.
-
-(* For [elements], [min_elt], [max_elt] and [choose], we would need setoid 
-   structures on [list elt] and [option elt]. *)
-
-(* Later:
-Add Morphism cardinal ; cardinal_m.
-*)
-
-End Facts.
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
deleted file mode 100644
index 5fa6c757f..000000000
--- a/theories/FSets/FSetWeakInterface.v
+++ /dev/null
@@ -1,264 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(** * Finite sets library *)
-
-(** Set interfaces for types with only a decidable equality, but no ordering *)
-
-Require Export Bool DecidableType.
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(** * Non-dependent signature
-
-    Signature [S] presents sets as purely informative programs 
-    together with axioms *)
-
-Module Type S.
-
-  (** The module E of base objects is meant to be a DecidableType
-     (and used to be so). But requiring only an EqualityType here
-     allows subtyping between FSet and FSetWeak *)
-  Declare Module E : EqualityType.
-  Definition elt := E.t.
-
-  Parameter t : Set. (** the abstract type of sets *)
-
-  (** Logical predicates *)
-  Parameter In : elt -> t -> Prop.
-  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.
-  
-  Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
-  Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
-
-  Parameter empty : t.
-  (** The empty set. *)
-
-  Parameter is_empty : t -> bool.
-  (** Test whether a set is empty or not. *)
-
-  Parameter mem : elt -> t -> bool.
-  (** [mem x s] tests whether [x] belongs to the set [s]. *)
-
-  Parameter add : elt -> t -> t.
-  (** [add x s] returns a set containing all elements of [s],
-  plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
-
-  Parameter singleton : elt -> t.
-  (** [singleton x] returns the one-element set containing only [x]. *)
-
-  Parameter remove : elt -> t -> t.
-  (** [remove x s] returns a set containing all elements of [s],
-  except [x]. If [x] was not in [s], [s] is returned unchanged. *)
-
-  Parameter union : t -> t -> t.
-  (** Set union. *)
-
-  Parameter inter : t -> t -> t.
-  (** Set intersection. *)
-
-  Parameter diff : t -> t -> t.
-  (** Set difference. *)
-
-  Definition eq : t -> t -> Prop := Equal.
-  (** EqualityType is a subset of this interface, but not 
-  DecidableType, in order to have FSetWeak < FSet. 
-  Hence no weak sets of weak sets in general, but it works 
-  at least with FSetWeakList.make that provides an eq_dec. *)
-
-  Parameter equal : t -> t -> bool.
-  (** [equal s1 s2] tests whether the sets [s1] and [s2] are
-  equal, that is, contain equal elements. *)
-
-  Parameter subset : t -> t -> bool.
-  (** [subset s1 s2] tests whether the set [s1] is a subset of
-  the set [s2]. *)
-
-  (** Coq comment: [iter] is useless in a purely functional world *)
-  (**  iter: (elt -> unit) -> set -> unit. i*)
-  (** [iter f s] applies [f] in turn to all elements of [s].
-  The order in which the elements of [s] are presented to [f]
-  is unspecified. *)
-
-  Parameter fold : forall A : Type, (elt -> A -> A) -> t -> A -> A.
-  (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
-  where [x1 ... xN] are the elements of [s].
-  The order in which elements of [s] are presented to [f] is
-  unspecified. *)
-
-  Parameter for_all : (elt -> bool) -> t -> bool.
-  (** [for_all p s] checks if all elements of the set
-  satisfy the predicate [p]. *)
-
-  Parameter exists_ : (elt -> bool) -> t -> bool.
-  (** [exists p s] checks if at least one element of
-  the set satisfies the predicate [p]. *)
-
-  Parameter filter : (elt -> bool) -> t -> t.
-  (** [filter p s] returns the set of all elements in [s]
-  that satisfy predicate [p]. *)
-
-  Parameter partition : (elt -> bool) -> t -> t * t.
-  (** [partition p s] returns a pair of sets [(s1, s2)], where
-  [s1] is the set of all the elements of [s] that satisfy the
-  predicate [p], and [s2] is the set of all the elements of
-  [s] that do not satisfy [p]. *)
-
-  Parameter cardinal : t -> nat.
-  (** Return the number of elements of a set. *)
-  (** Coq comment: nat instead of int ... *)
-
-  Parameter elements : t -> list elt.
-  (** Return the list of all elements of the given set, in any order. *)
-
-  Parameter choose : t -> option elt.
-  (** Return one element of the given set, or raise [Not_found] if
-  the set is empty. Which element is chosen is unspecified.
-  Equal sets could return different elements. *)
-  (** Coq comment: [Not_found] is represented by the option type *)
-
-  Section Spec. 
-
-  Variable s s' s'': t.
-  Variable x y : elt.
-
-  (** Specification of [In] *)
-  Parameter In_1 : E.eq x y -> In x s -> In y s.
-
-  (** Specification of [eq] *)
-  Parameter eq_refl : eq s s. 
-  Parameter eq_sym : eq s s' -> eq s' s.
-  Parameter eq_trans : eq s s' -> eq s' s'' -> eq s s''.
-
-  (** Specification of [mem] *)
-  Parameter mem_1 : In x s -> mem x s = true.
-  Parameter mem_2 : mem x s = true -> In x s. 
- 
-  (** Specification of [equal] *) 
-  Parameter equal_1 : Equal s s' -> equal s s' = true.
-  Parameter equal_2 : equal s s' = true -> Equal s s'.
-
-  (** Specification of [subset] *)
-  Parameter subset_1 : Subset s s' -> subset s s' = true.
-  Parameter subset_2 : subset s s' = true -> Subset s s'.
-
-  (** Specification of [empty] *)
-  Parameter empty_1 : Empty empty.
-
-  (** Specification of [is_empty] *)
-  Parameter is_empty_1 : Empty s -> is_empty s = true. 
-  Parameter is_empty_2 : is_empty s = true -> Empty s.
- 
-  (** Specification of [add] *)
-  Parameter add_1 : E.eq x y -> In y (add x s).
-  Parameter add_2 : In y s -> In y (add x s).
-  Parameter add_3 : ~ E.eq x y -> In y (add x s) -> In y s. 
-
-  (** Specification of [remove] *)
-  Parameter remove_1 : E.eq x y -> ~ In y (remove x s).
-  Parameter remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
-  Parameter remove_3 : In y (remove x s) -> In y s.
-
-  (** Specification of [singleton] *)
-  Parameter singleton_1 : In y (singleton x) -> E.eq x y. 
-  Parameter singleton_2 : E.eq x y -> In y (singleton x). 
-
-  (** Specification of [union] *)
-  Parameter union_1 : In x (union s s') -> In x s \/ In x s'.
-  Parameter union_2 : In x s -> In x (union s s'). 
-  Parameter union_3 : In x s' -> In x (union s s').
-
-  (** Specification of [inter] *)
-  Parameter inter_1 : In x (inter s s') -> In x s.
-  Parameter inter_2 : In x (inter s s') -> In x s'.
-  Parameter inter_3 : In x s -> In x s' -> In x (inter s s').
-
-  (** Specification of [diff] *)
-  Parameter diff_1 : In x (diff s s') -> In x s. 
-  Parameter diff_2 : In x (diff s s') -> ~ In x s'.
-  Parameter diff_3 : In x s -> ~ In x s' -> In x (diff s s').
- 
-  (** Specification of [fold] *)  
-  Parameter fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
-      fold f s i = fold_left (fun a e => f e a) (elements s) i.
-
-  (** Specification of [cardinal] *)  
-  Parameter cardinal_1 : cardinal s = length (elements s).
-
-  Section Filter.
-  
-  Variable f : elt -> bool.
-
-  (** Specification of [filter] *)
-  Parameter filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. 
-  Parameter filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. 
-  Parameter filter_3 :
-      compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
-
-  (** Specification of [for_all] *)
-  Parameter for_all_1 :
-      compat_bool E.eq f ->
-      For_all (fun x => f x = true) s -> for_all f s = true.
-  Parameter for_all_2 :
-      compat_bool E.eq f ->
-      for_all f s = true -> For_all (fun x => f x = true) s.
-
-  (** Specification of [exists] *)
-  Parameter exists_1 :
-      compat_bool E.eq f ->
-      Exists (fun x => f x = true) s -> exists_ f s = true.
-  Parameter exists_2 :
-      compat_bool E.eq f ->
-      exists_ f s = true -> Exists (fun x => f x = true) s.
-
-  (** Specification of [partition] *)
-  Parameter partition_1 :
-      compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
-  Parameter partition_2 :
-      compat_bool E.eq f ->
-      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
-
-  End Filter.
-
-  (** Specification of [elements] *)
-  Parameter elements_1 : In x s -> InA E.eq x (elements s).
-  Parameter elements_2 : InA E.eq x (elements s) -> In x s.
-  (** When compared with ordered FSet, here comes the only 
-      property that is really weaker: *)
-  Parameter elements_3w : NoDupA E.eq (elements s).
-
-  (** Specification of [choose] *)
-  Parameter choose_1 : choose s = Some x -> In x s.
-  Parameter choose_2 : choose s = None -> Empty s.
-
-  End Spec.
-
-  Hint Resolve mem_1 equal_1 subset_1 empty_1
-    is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
-    remove_2 singleton_2 union_1 union_2 union_3
-    inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
-    partition_1 partition_2 elements_1 elements_3w 
-    : set.
-  Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
-    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
-    filter_1 filter_2 for_all_2 exists_2 elements_2 
-    : set.
-  (* for compatibility with earlier hints *)
-  Hint Resolve In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
-    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
-    filter_1 filter_2 for_all_2 exists_2 elements_2 
-    : oldset.
-
-
-End S.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index b207f1f1e..c692950e0 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -13,7 +13,7 @@
 (** This file proposes an implementation of the non-dependant 
     interface [FSetWeakInterface.S] using lists without redundancy. *)
 
-Require Import FSetWeakInterface.
+Require Import FSetInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -804,7 +804,7 @@ 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) <: WS with Module E := X.
 
  Module Raw := Raw X. 
  Module E := X.
diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v
deleted file mode 100644
index 3a8bdb032..000000000
--- a/theories/FSets/FSetWeakProperties.v
+++ /dev/null
@@ -1,771 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(** * Finite sets library *)
-
-(** This functor derives additional properties from [FSetWeakInterface.S].
-    Contrary to the functor in [FSetWeakEqProperties] it uses 
-    predicates over sets instead of sets operations, i.e.
-    [In x s] instead of [mem x s=true], 
-    [Equal s s'] instead of [equal s s'=true], etc. *)
-
-Require Export FSetWeakInterface. 
-Require Import FSetWeakFacts FSetDecide.
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-Hint Unfold transpose compat_op.
-Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence.
-
-Module Properties 
- (M:FSetWeakInterface.S)
- (D:DecidableType with Definition t:=M.E.t 
-                  with Definition eq:=M.E.eq).
-  Module Import FM := Facts M D.
-  Module Import Dec := FSetDecide.WeakDecide M D.
-  Import M.E.
-  Import M.
-
-  Lemma In_dec : forall x s, {In x s} + {~ In x s}.
-  Proof.
-  intros; generalize (mem_iff s x); case (mem x s); intuition.
-  Qed.
-
-  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
-
-  Lemma Add_Equal : forall x s s', Add x s s' <-> s' [=] add x s.
-  Proof.
-  unfold Add.
-  split; intros.
-  red; intros.
-  rewrite H; clear H.
-  fsetdec.
-  fsetdec.
-  Qed.
-  
-  Ltac expAdd := repeat rewrite Add_Equal.
-
-  Section BasicProperties.
-
-  Variable s s' s'' s1 s2 s3 : t.
-  Variable x x' : elt.
-
-  Lemma equal_refl : s[=]s.
-  Proof. fsetdec. Qed.
-
-  Lemma equal_sym : s[=]s' -> s'[=]s.
-  Proof. fsetdec. Qed.
-
-  Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3.
-  Proof. fsetdec. Qed.
-
-  Lemma subset_refl : s[<=]s. 
-  Proof. fsetdec. Qed.
-
-  Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
-  Proof. fsetdec. Qed.
-
-  Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
-  Proof. fsetdec. Qed.
-
-  Lemma subset_equal : s[=]s' -> s[<=]s'.
-  Proof. fsetdec. Qed.
-
-  Lemma subset_empty : empty[<=]s.
-  Proof. fsetdec. Qed.
-
-  Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2.
-  Proof. fsetdec. Qed.
-
-  Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3.
-  Proof. fsetdec. Qed.
- 
-  Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2.
-  Proof. fsetdec. Qed.
-
-  Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2.
-  Proof. fsetdec. Qed.
-
-  Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.
-  Proof. fsetdec. Qed.
- 
-  Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
-  Proof. intuition fsetdec. Qed.
-
-  Lemma empty_is_empty_1 : Empty s -> s[=]empty.
-  Proof. fsetdec. Qed.
-
-  Lemma empty_is_empty_2 : s[=]empty -> Empty s.
-  Proof. fsetdec. Qed.
-
-  Lemma add_equal : In x s -> add x s [=] s.
-  Proof. fsetdec. Qed.
- 
-  Lemma add_add : add x (add x' s) [=] add x' (add x s).
-  Proof. fsetdec. Qed.
-
-  Lemma remove_equal : ~ In x s -> remove x s [=] s.
-  Proof. fsetdec. Qed.
-
-  Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.
-  Proof. fsetdec. Qed.
-
-  Lemma add_remove : In x s -> add x (remove x s) [=] s.
-  Proof. fsetdec. Qed.
-
-  Lemma remove_add : ~In x s -> remove x (add x s) [=] s.
-  Proof. fsetdec. Qed.
-
-  Lemma singleton_equal_add : singleton x [=] add x empty.
-  Proof. fsetdec. Qed.
-
-  Lemma union_sym : union s s' [=] union s' s.
-  Proof. fsetdec. Qed.
-
-  Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'.
-  Proof. fsetdec. Qed.
-
-  Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.
-  Proof. fsetdec. Qed.
-
-  Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.
-  Proof. fsetdec. Qed.
-
-  Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
-  Proof. fsetdec. Qed.
-
-  Lemma add_union_singleton : add x s [=] union (singleton x) s.
-  Proof. fsetdec. Qed.
-
-  Lemma union_add : union (add x s) s' [=] add x (union s s').
-  Proof. fsetdec. Qed.
-
-  Lemma union_remove_add_1 : 
-   union (remove x s) (add x s') [=] union (add x s) (remove x s').
-  Proof. fsetdec. Qed.
-
-  Lemma union_remove_add_2 : In x s -> 
-   union (remove x s) (add x s') [=] union s s'.
-  Proof. fsetdec. Qed.
-
-  Lemma union_subset_1 : s [<=] union s s'.
-  Proof. fsetdec. Qed.
-
-  Lemma union_subset_2 : s' [<=] union s s'.
-  Proof. fsetdec. Qed.
-
-  Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''.
-  Proof. fsetdec. Qed.
-
-  Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.
-  Proof. fsetdec. Qed. 
-
-  Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.
-  Proof. fsetdec. Qed. 
-
-  Lemma empty_union_1 : Empty s -> union s s' [=] s'.
-  Proof. fsetdec. Qed.
-
-  Lemma empty_union_2 : Empty s -> union s' s [=] s'.
-  Proof. fsetdec. Qed.
-
-  Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s'). 
-  Proof. fsetdec. Qed.
-
-  Lemma inter_sym : inter s s' [=] inter s' s.
-  Proof. fsetdec. Qed.
-
-  Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s.
-  Proof. fsetdec. Qed.
-
-  Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.
-  Proof. fsetdec. Qed.
-
-  Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.
-  Proof. fsetdec. Qed.
-
-  Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
-  Proof. fsetdec. Qed.
-
-  Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s'').
-  Proof. fsetdec. Qed.
-
-  Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s'').
-  Proof. fsetdec. Qed.
-
-  Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s').
-  Proof. fsetdec. Qed.
-
-  Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'.
-  Proof. fsetdec. Qed.
-
-  Lemma empty_inter_1 : Empty s -> Empty (inter s s').
-  Proof. fsetdec. Qed.
-
-  Lemma empty_inter_2 : Empty s' -> Empty (inter s s').
-  Proof. fsetdec. Qed.
-
-  Lemma inter_subset_1 : inter s s' [<=] s.
-  Proof. fsetdec. Qed.
-
-  Lemma inter_subset_2 : inter s s' [<=] s'.
-  Proof. fsetdec. Qed.
-
-  Lemma inter_subset_3 :
-   s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'.
-  Proof. fsetdec. Qed.
-
-  Lemma empty_diff_1 : Empty s -> Empty (diff s s'). 
-  Proof. fsetdec. Qed.
-
-  Lemma empty_diff_2 : Empty s -> diff s' s [=] s'.
-  Proof. fsetdec. Qed.
-
-  Lemma diff_subset : diff s s' [<=] s.
-  Proof. fsetdec. Qed.
-
-  Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty.
-  Proof. fsetdec. Qed.
-
-  Lemma remove_diff_singleton :
-   remove x s [=] diff s (singleton x).
-  Proof. fsetdec. Qed.
-
-  Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty. 
-  Proof. fsetdec. Qed.
-
-  Lemma diff_inter_all : union (diff s s') (inter s s') [=] s.
-  Proof. fsetdec. Qed.
-
-  Lemma Add_add : Add x s (add x s).
-  Proof. expAdd; fsetdec. Qed.
-
-  Lemma Add_remove : In x s -> Add x (remove x s) s. 
-  Proof. expAdd; fsetdec. Qed.
-
-  Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s'').
-  Proof. expAdd; fsetdec. Qed. 
-
-  Lemma inter_Add :
-   In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'').
-  Proof. expAdd; fsetdec. Qed. 
-
-  Lemma union_Equal :
-   In x s'' -> Add x s s' -> union s s'' [=] union s' s''.
-  Proof. expAdd; fsetdec. Qed. 
-
-  Lemma inter_Add_2 :
-   ~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''.
-  Proof. expAdd; fsetdec. Qed.
-
-  End BasicProperties.
-
-  Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
-  Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym 
-    subset_trans subset_empty subset_remove_3 subset_diff subset_add_3 
-    subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
-    remove_equal singleton_equal_add union_subset_equal union_equal_1 
-    union_equal_2 union_assoc add_union_singleton union_add union_subset_1 
-    union_subset_2 union_subset_3 inter_subset_equal inter_equal_1 inter_equal_2
-    inter_assoc union_inter_1 union_inter_2 inter_add_1 inter_add_2
-    empty_inter_1 empty_inter_2 empty_union_1 empty_union_2 empty_diff_1 
-    empty_diff_2 union_Add inter_Add union_Equal inter_Add_2 not_in_union 
-    inter_subset_1 inter_subset_2 inter_subset_3 diff_subset diff_subset_equal 
-    remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
-    Equal_remove add_add : set.
-
-  (** * Properties of elements *)
-
-  Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
-  Proof.
-  intros.
-  unfold Empty.
-  split; intros.
-  assert (forall a, ~ List.In a (elements s)).
-   red; intros.
-   apply (H a).
-   rewrite elements_iff.
-   rewrite InA_alt; exists a; auto.
-  destruct (elements s); auto.
-  elim (H0 e); simpl; auto.
-  red; intros.
-  rewrite elements_iff in H0.
-  rewrite InA_alt in H0; destruct H0.
-  rewrite H in H0; destruct H0 as (_,H0); inversion H0.
-  Qed.
-
-  (** * Alternative (weaker) specifications for [fold] *)
-
-  Section Old_Spec_Now_Properties. 
-
-  Notation NoDup := (NoDupA E.eq).
-
-  (** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
-        takes the set elements was unspecified. This specification reflects this fact: 
-  *)
-
-  Lemma fold_0 : 
-      forall s (A : Set) (i : A) (f : elt -> A -> A),
-      exists l : list elt,
-        NoDup l /\
-        (forall x : elt, In x s <-> InA E.eq x l) /\
-        fold f s i = fold_right f i l.
-  Proof.
-  intros; exists (rev (elements s)); split.
-  apply NoDupA_rev; auto with set.
-  exact E.eq_trans.
-  split; intros.
-  rewrite elements_iff; do 2 rewrite InA_alt.
-  split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
-  rewrite fold_left_rev_right.
-  apply fold_1.
-  Qed.
-
-  (** An alternate (and previous) specification for [fold] was based on 
-      the recursive structure of a set. It is now lemmas [fold_1] and 
-      [fold_2]. *)
-
-  Lemma fold_1 :
-   forall s (A : Set) (eqA : A -> A -> Prop) 
-     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
-   Empty s -> eqA (fold f s i) i.
-  Proof.
-  unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))).
-  rewrite H3; clear H3.
-  generalize H H2; clear H H2; case l; simpl; intros.
-  refl_st.
-  elim (H e).
-  elim (H2 e); intuition. 
-  Qed.
-
-  Lemma fold_2 :
-   forall s s' x (A : Set) (eqA : A -> A -> Prop)
-     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
-   compat_op E.eq eqA f ->
-   transpose eqA f ->
-   ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
-  Proof.
-  intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); 
-    destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
-  rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
-  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
-  eauto.
-  rewrite <- Hl1; auto.
-  intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1; 
-   rewrite (H2 a); intuition.
-  Qed.
-
-  (** In fact, [fold] on empty sets is more than equivalent to 
-      the initial element, it is Leibniz-equal to it. *)
-
-  Lemma fold_1b :
-   forall s (A : Set)(i : A) (f : elt -> A -> A),
-   Empty s -> (fold f s i) = i.
-  Proof.
-  intros.
-  rewrite M.fold_1.
-  rewrite elements_Empty in H; rewrite H; simpl; auto.
-  Qed.
-
-  (** Similar specifications for [cardinal]. *)
-
-  Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
-  Proof.
-  intros; rewrite cardinal_1; rewrite M.fold_1.
-  symmetry; apply fold_left_length; auto.
-  Qed.
-
-  Lemma cardinal_0 :
-     forall s, exists l : list elt,
-        NoDupA E.eq l /\
-        (forall x : elt, In x s <-> InA E.eq x l) /\ 
-        cardinal s = length l.
-  Proof. 
-  intros; exists (elements s); intuition; apply cardinal_1.
-  Qed.
-
-  Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
-  Proof.
-  intros; rewrite cardinal_fold; apply fold_1; auto.
-  Qed.
-
-  Lemma cardinal_2 :
-    forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).
-  Proof.
-  intros; do 2 rewrite cardinal_fold.
-  change S with ((fun _ => S) x).
-  apply fold_2; auto.
-  Qed.
-
-  End Old_Spec_Now_Properties.
-
-  (** * Induction principle over sets *)
-
-  Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
-  Proof.
-  intros.
-  rewrite elements_Empty, M.cardinal_1.
-  destruct (elements s); intuition; discriminate.
-  Qed.
-
-  Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s. 
-  Proof.
-  intros; rewrite cardinal_Empty; auto. 
-  Qed.
-  Hint Resolve cardinal_inv_1.
- 
-  Lemma cardinal_inv_2 :
-   forall s n, cardinal s = S n -> { x : elt | In x s }.
-  Proof. 
-  intros; rewrite M.cardinal_1 in H.
-  generalize (elements_2 (s:=s)).
-  destruct (elements s); try discriminate. 
-  exists e; auto.
-  Qed.
-
-  Lemma cardinal_inv_2b :
-   forall s, cardinal s <> 0 -> { x : elt | In x s }.
-  Proof.
-  intro; generalize (@cardinal_inv_2 s); destruct cardinal; 
-   [intuition|eauto].
-  Qed.
-
-  Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
-  Proof. 
-  symmetry.
-  remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H.
-  induction n; intros.
-  apply cardinal_1; rewrite <- H; auto.
-  destruct (cardinal_inv_2 Heqn) as (x,H2).
-  revert Heqn.
-  rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.
-  rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set.
-  Qed.    
-
-  Add Morphism cardinal : cardinal_m.
-  Proof.
-  exact Equal_cardinal.
-  Qed.
-
-  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
-
-  Lemma set_induction :
-   forall P : t -> Type,
-   (forall s : t, Empty s -> P s) ->
-   (forall s s' : t, P s -> forall x : elt, ~In x s -> Add x s s' -> P s') ->
-   forall s : t, P s.
-  Proof.
-  intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
-  destruct (cardinal_inv_2 (sym_eq Heqn)) as (x,H0). 
-  apply X0 with (remove x s) x; auto with set.
-  apply IHn; auto.
-  assert (S n = S (cardinal (remove x s))).
-    rewrite Heqn; apply cardinal_2 with x; auto with set.
-  inversion H; auto.
-  Qed.
-
-  (** Other properties of [fold]. *)
-
-  Section Fold. 
-  Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
-  Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
-
-  Section Fold_1. 
-  Variable i i':A.
-
-  Lemma fold_empty : (fold f empty i) = i.
-  Proof. 
-  apply fold_1b; auto with set.
-  Qed.
-
-  Lemma fold_equal : 
-   forall s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
-  Proof. 
-  intros s; pattern s; apply set_induction; clear s; intros.
-  trans_st i.
-  apply fold_1; auto.
-  sym_st; apply fold_1; auto.
-  rewrite <- H0; auto.
-  trans_st (f x (fold f s i)).
-  apply fold_2 with (eqA := eqA); auto.
-  sym_st; apply fold_2 with (eqA := eqA); auto.
-  unfold Add in *; intros.
-  rewrite <- H2; auto.
-  Qed.
-   
-  Lemma fold_add : forall s x, ~In x s -> 
-   eqA (fold f (add x s) i) (f x (fold f s i)).
-  Proof. 
-  intros; apply fold_2 with (eqA := eqA); auto.
-  Qed.
-
-  Lemma add_fold : forall s x, In x s -> 
-   eqA (fold f (add x s) i) (fold f s i).
-  Proof.
-  intros; apply fold_equal; auto with set.
-  Qed.
-
-  Lemma remove_fold_1: forall s x, In x s -> 
-   eqA (f x (fold f (remove x s) i)) (fold f s i).
-  Proof.
-  intros.
-  sym_st.
-  apply fold_2 with (eqA:=eqA); auto with set.
-  Qed.
-
-  Lemma remove_fold_2: forall s x, ~In x s -> 
-   eqA (fold f (remove x s) i) (fold f s i).
-  Proof.
-  intros.
-  apply fold_equal; auto with set.
-  Qed.
-
-  Lemma fold_commutes : forall s x, 
-   eqA (fold f s (f x i)) (f x (fold f s i)).
-  Proof.
-  intros; pattern s; apply set_induction; clear s; intros.
-  trans_st (f x i).
-  apply fold_1; auto.
-  sym_st.
-  apply Comp; auto.
-  apply fold_1; auto.
-  trans_st (f x0 (fold f s (f x i))).
-  apply fold_2 with (eqA:=eqA); auto.
-  trans_st (f x0 (f x (fold f s i))).
-  trans_st (f x (f x0 (fold f s i))).
-  apply Comp; auto.
-  sym_st.
-  apply fold_2 with (eqA:=eqA); auto.
-  Qed.
-
-  Lemma fold_init : forall s, eqA i i' -> 
-   eqA (fold f s i) (fold f s i').
-  Proof. 
-  intros; pattern s; apply set_induction; clear s; intros.
-  trans_st i.
-  apply fold_1; auto.
-  trans_st i'.
-  sym_st; apply fold_1; auto.
-  trans_st (f x (fold f s i)).
-  apply fold_2 with (eqA:=eqA); auto.
-  trans_st (f x (fold f s i')).
-  sym_st; apply fold_2 with (eqA:=eqA); auto.
-  Qed.
-
-  End Fold_1.
-  Section Fold_2.
-  Variable i:A.
-
-  Lemma fold_union_inter : forall s s',
-   eqA (fold f (union s s') (fold f (inter s s') i))
-       (fold f s (fold f s' i)).
-  Proof.
-  intros; pattern s; apply set_induction; clear s; intros.
-  trans_st (fold f s' (fold f (inter s s') i)).
-  apply fold_equal; auto with set.
-  trans_st (fold f s' i).
-  apply fold_init; auto.
-  apply fold_1; auto with set.
-  sym_st; apply fold_1; auto.
-  rename s'0 into s''.
-  destruct (In_dec x s').
-  (* In x s' *)   
-  trans_st (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set.
-  apply fold_init; auto.
-  apply fold_2 with (eqA:=eqA); auto with set.
-  rewrite inter_iff; intuition.
-  trans_st (f x (fold f s (fold f s' i))).
-  trans_st (fold f (union s s') (f x (fold f (inter s s') i))).
-  apply fold_equal; auto.
-  apply equal_sym; apply union_Equal with x; auto with set.
-  trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
-  apply fold_commutes; auto.
-  sym_st; apply fold_2 with (eqA:=eqA); auto.
-  (* ~(In x s') *)
-  trans_st (f x (fold f (union s s') (fold f (inter s'' s') i))).
-  apply fold_2 with (eqA:=eqA); auto with set.
-  trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
-  apply Comp;auto.
-  apply fold_init;auto.
-  apply fold_equal;auto.
-  apply equal_sym; apply inter_Add_2 with x; auto with set.
-  trans_st (f x (fold f s (fold f s' i))).
-  sym_st; apply fold_2 with (eqA:=eqA); auto.
-  Qed.
-
-  End Fold_2.
-  Section Fold_3.
-  Variable i:A.
-
-  Lemma fold_diff_inter : forall s s', 
-   eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
-  Proof.
-  intros.
-  trans_st (fold f (union (diff s s') (inter s s')) 
-              (fold f (inter (diff s s') (inter s s')) i)).
-  sym_st; apply fold_union_inter; auto.
-  trans_st (fold f s (fold f (inter (diff s s') (inter s s')) i)).
-  apply fold_equal; auto with set.
-  apply fold_init; auto.
-  apply fold_1; auto with set.
-  Qed.
-
-  Lemma fold_union: forall s s', 
-   (forall x, ~(In x s/\In x s')) ->
-   eqA (fold f (union s s') i) (fold f s (fold f s' i)).
-  Proof.
-  intros.
-  trans_st (fold f (union s s') (fold f (inter s s') i)).
-  apply fold_init; auto.
-  sym_st; apply fold_1; auto with set.
-  unfold Empty; intro a; generalize (H a); set_iff; tauto.
-  apply fold_union_inter; auto.
-  Qed.
-
-  End Fold_3.
-  End Fold.
-
-  Lemma fold_plus :
-   forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
-  Proof.
-  assert (st := gen_st nat).
-  assert (fe : compat_op E.eq (@Logic.eq _) (fun _ => S)) by (unfold compat_op; auto). 
-  assert (fp : transpose (@Logic.eq _) (fun _:elt => S)) by (unfold transpose; auto).
-  intros s p; pattern s; apply set_induction; clear s; intros.
-  rewrite (fold_1 st p (fun _ => S) H).
-  rewrite (fold_1 st 0 (fun _ => S) H); trivial.
-  assert (forall p s', Add x s s' -> fold (fun _ => S) s' p = S (fold (fun _ => S) s p)).
-   change S with ((fun _ => S) x).  
-   intros; apply fold_2; auto.
-  rewrite H2; auto.
-  rewrite (H2 0); auto.
-  rewrite H.
-  simpl; auto.
-  Qed.
-
-  (** more properties of [cardinal] *)
-
-  Lemma empty_cardinal : cardinal empty = 0.
-  Proof.
-  rewrite cardinal_fold; apply fold_1; auto with set.
-  Qed.
-
-  Hint Immediate empty_cardinal cardinal_1 : set.
-
-  Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
-  Proof.
-  intros.
-  rewrite (singleton_equal_add x).
-  replace 0 with (cardinal empty); auto with set.
-  apply cardinal_2 with x; auto with set.
-  Qed.
-
-  Hint Resolve singleton_cardinal: set.
-
-  Lemma diff_inter_cardinal :
-   forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s .
-  Proof.
-  intros; do 3 rewrite cardinal_fold.
-  rewrite <- fold_plus.
-  apply fold_diff_inter with (eqA:=@Logic.eq nat); auto.
-  Qed.
-
-  Lemma union_cardinal: 
-   forall s s', (forall x, ~(In x s/\In x s')) -> 
-   cardinal (union s s')=cardinal s+cardinal s'.
-  Proof.
-  intros; do 3 rewrite cardinal_fold.
-  rewrite <- fold_plus.
-  apply fold_union; auto.
-  Qed.
-
-  Lemma subset_cardinal : 
-   forall s s', s[<=]s' -> cardinal s <= cardinal s' .
-  Proof.
-  intros.
-  rewrite <- (diff_inter_cardinal s' s).
-  rewrite (inter_sym s' s).
-  rewrite (inter_subset_equal H); auto with arith.
-  Qed.
-
-  Lemma subset_cardinal_lt : 
-   forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.
-  Proof. 
-  intros.
-  rewrite <- (diff_inter_cardinal s' s).
-  rewrite (inter_sym s' s).
-  rewrite (inter_subset_equal H).
-  generalize (@cardinal_inv_1 (diff s' s)).
-  destruct (cardinal (diff s' s)).
-  intro H2; destruct (H2 (refl_equal _) x).
-  set_iff; auto.
-  intros _.
-  change (0 + cardinal s < S n + cardinal s).
-  apply Plus.plus_lt_le_compat; auto with arith.
-  Qed. 
-
-  Theorem union_inter_cardinal :
-   forall s s', cardinal (union s s') + cardinal (inter s s')  = cardinal s  + cardinal s' .
-  Proof.
-  intros.
-  do 4 rewrite cardinal_fold.
-  do 2 rewrite <- fold_plus.
-  apply fold_union_inter with (eqA:=@Logic.eq nat); auto.
-  Qed.
-
-  Lemma union_cardinal_inter : 
-   forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
-  Proof.
-  intros.
-  rewrite <- union_inter_cardinal.
-  rewrite Plus.plus_comm.
-  auto with arith.
-  Qed.
-
-  Lemma union_cardinal_le : 
-   forall s s', cardinal (union s s') <= cardinal s  + cardinal s'.
-  Proof.
-   intros; generalize (union_inter_cardinal s s').
-   intros; rewrite <- H; auto with arith.
-  Qed.
-
-  Lemma add_cardinal_1 : 
-   forall s x, In x s -> cardinal (add x s) = cardinal s.
-  Proof.
-  auto with set.  
-  Qed.
-
-  Lemma add_cardinal_2 :
-   forall s x, ~In x s -> cardinal (add x s) = S (cardinal s).
-  Proof.
-  intros.
-  do 2 rewrite cardinal_fold.
-  change S with ((fun _ => S) x);
-   apply fold_add with (eqA:=@Logic.eq nat); auto.
-  Qed.
-
-  Lemma remove_cardinal_1 :
-   forall s x, In x s -> S (cardinal (remove x s)) = cardinal s.
-  Proof.
-  intros.
-  do 2 rewrite cardinal_fold.
-  change S with ((fun _ =>S) x).
-  apply remove_fold_1 with (eqA:=@Logic.eq nat); auto.
-  Qed.
-
-  Lemma remove_cardinal_2 : 
-   forall s x, ~In x s -> cardinal (remove x s) = cardinal s.
-  Proof. 
-  auto with set.
-  Qed.
-
-  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
-
-End Properties.
diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v
index 6751eb427..012c0d60b 100644
--- a/theories/FSets/FSets.v
+++ b/theories/FSets/FSets.v
@@ -11,8 +11,11 @@
 Require Export OrderedType.
 Require Export OrderedTypeEx.
 Require Export OrderedTypeAlt.
+Require Export DecidableType.
+Require Export DecidableTypeEx.
 Require Export FSetInterface.
 Require Export FSetBridge.
 Require Export FSetProperties.
 Require Export FSetEqProperties.
+Require Export FSetWeakList.
 Require Export FSetList.