FSets, mais pas compile' par make world

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

11 files changed, 6296 insertions, 1 deletions

diff --git a/.depend.coq b/.depend.coq
index df150c945f..50e69b3de6 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -153,6 +153,12 @@ theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theo
 theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo
 theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
 theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo
+theories/FSets/FSet.vo: theories/FSets/FSet.v theories/FSets/FSetInterface.vo theories/FSets/FSetBridge.vo theories/FSets/FSetProperties.vo theories/FSets/FSetList.vo theories/FSets/FSetRBT.vo
+theories/FSets/FSetList.vo: theories/FSets/FSetList.v theories/FSets/FSetInterface.vo
+theories/FSets/FSetBridge.vo: theories/FSets/FSetBridge.v theories/FSets/FSetInterface.vo
+theories/FSets/FSetProperties.vo: theories/FSets/FSetProperties.v contrib/omega/Omega.vo theories/FSets/FSetInterface.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Bool/Zerob.vo
+theories/FSets/FSetInterface.vo: theories/FSets/FSetInterface.v theories/Bool/Bool.vo theories/Lists/PolyList.vo theories/Sorting/Sorting.vo theories/Setoids/Setoid.vo
+theories/FSets/FSetRBT.vo: theories/FSets/FSetRBT.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/FSets/FSetBridge.vo contrib/omega/Omega.vo theories/ZArith/ZArith.vo
 theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
 theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo
 theories/IntMap/Addec.vo: theories/IntMap/Addec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/ZArith/ZArith.vo theories/IntMap/Addr.vo
diff --git a/.depend.newcoq b/.depend.newcoq
index 9cdc3b1da4..70a37e7d3c 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -153,6 +153,12 @@ newtheories/Sets/Multiset.vo: newtheories/Sets/Multiset.v newtheories/Sets/Permu
 newtheories/Sets/Relations_3_facts.vo: newtheories/Sets/Relations_3_facts.v newtheories/Sets/Relations_1.vo newtheories/Sets/Relations_1_facts.vo newtheories/Sets/Relations_2.vo newtheories/Sets/Relations_2_facts.vo newtheories/Sets/Relations_3.vo
 newtheories/Sets/Partial_Order.vo: newtheories/Sets/Partial_Order.v newtheories/Sets/Ensembles.vo newtheories/Sets/Relations_1.vo
 newtheories/Sets/Uniset.vo: newtheories/Sets/Uniset.v newtheories/Bool/Bool.vo newtheories/Sets/Permut.vo
+newtheories/FSets/FSet.vo: newtheories/FSets/FSet.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetBridge.vo newtheories/FSets/FSetProperties.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetRBT.vo
+newtheories/FSets/FSetList.vo: newtheories/FSets/FSetList.v newtheories/FSets/FSetInterface.vo
+newtheories/FSets/FSetBridge.vo: newtheories/FSets/FSetBridge.v newtheories/FSets/FSetInterface.vo
+newtheories/FSets/FSetProperties.vo: newtheories/FSets/FSetProperties.v newcontrib/omega/Omega.vo newtheories/FSets/FSetInterface.vo newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Bool/Zerob.vo
+newtheories/FSets/FSetInterface.vo: newtheories/FSets/FSetInterface.v newtheories/Bool/Bool.vo newtheories/Lists/PolyList.vo newtheories/Sorting/Sorting.vo newtheories/Setoids/Setoid.vo
+newtheories/FSets/FSetRBT.vo: newtheories/FSets/FSetRBT.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetBridge.vo newcontrib/omega/Omega.vo newtheories/ZArith/ZArith.vo
 newtheories/IntMap/Adalloc.vo: newtheories/IntMap/Adalloc.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/Arith/Arith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Fset.vo
 newtheories/IntMap/Mapcanon.vo: newtheories/IntMap/Mapcanon.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Arith/Arith.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo newtheories/IntMap/Adist.vo newtheories/IntMap/Addec.vo newtheories/IntMap/Map.vo newtheories/IntMap/Mapaxioms.vo newtheories/IntMap/Mapiter.vo newtheories/IntMap/Fset.vo newtheories/Lists/PolyList.vo newtheories/IntMap/Lsort.vo newtheories/IntMap/Mapsubset.vo newtheories/IntMap/Mapcard.vo
 newtheories/IntMap/Addec.vo: newtheories/IntMap/Addec.v newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/ZArith/ZArith.vo newtheories/IntMap/Addr.vo
diff --git a/Makefile b/Makefile
index 600b3546cb..6b1409a9b9 100644
--- a/Makefile
+++ b/Makefile
@@ -594,6 +594,10 @@ SETSVO=theories/Sets/Classical_sets.vo     theories/Sets/Permut.vo \
  theories/Sets/Multiset.vo          theories/Sets/Relations_3_facts.vo \
  theories/Sets/Partial_Order.vo     theories/Sets/Uniset.vo
 
+FSETSVO=theories/FSets/FSet.vo            theories/FSets/FSetList.vo \
+	theories/FSets/FSetBridge.vo      theories/FSets/FSetProperties.vo \
+	theories/FSets/FSetInterface.vo   theories/FSets/FSetRBT.vo 
+
 INTMAPVO=theories/IntMap/Adalloc.vo    theories/IntMap/Mapcanon.vo \
 theories/IntMap/Addec.vo      theories/IntMap/Mapcard.vo \
 theories/IntMap/Addr.vo       theories/IntMap/Mapc.vo \
@@ -678,6 +682,7 @@ bool: $(BOOLVO)
 zarith: $(ZARITHVO)
 lists: $(LISTSVO)
 sets: $(SETSVO)
+fsets: $(FSETSVO)
 intmap: $(INTMAPVO)
 relations: $(RELATIONSVO)
 wellfounded: $(WELLFOUNDEDVO)
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index d17741295b..40e1f4a680 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -503,3 +503,38 @@ Lemma absoption_orb : (b1,b2:bool)
 Proof.
   NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
 Qed.
+
+
+(** Misc. equalities between booleans (to be used by Auto) *)
+
+Lemma bool_1 : (b1,b2:bool)(b1=true <-> b2=true) -> b1=b2. 
+Proof. 
+ Intros b1 b2; Case b1; Case b2; Intuition.
+Qed.
+
+Lemma bool_2 : (b1,b2:bool)b1=b2 -> b1=true -> b2=true.
+Proof. 
+ Intros b1 b2; Case b1; Case b2; Intuition.
+Qed. 
+
+Lemma bool_3 : (b:bool) ~(negb b)=true -> b=true.
+Proof.
+  Induction b; Intuition.
+Qed.
+
+Lemma bool_4 : (b:bool) b=true -> ~(negb b)=true.  
+Proof.
+  Induction b; Intuition.
+Qed.
+
+Lemma bool_5 : (b:bool) (negb b)=true -> ~b=true.
+Proof.
+  Induction b; Intuition.
+Qed.
+
+Lemma bool_6 : (b:bool) ~b=true -> (negb b)=true.  
+Proof.
+  Induction b; Intuition.
+Qed.
+
+Hints Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6.
diff --git a/theories/FSets/FSet.v b/theories/FSets/FSet.v
new file mode 100644
index 0000000000..50f3799ed3
--- /dev/null
+++ b/theories/FSets/FSet.v
@@ -0,0 +1,16 @@
+(***********************************************************************)
+(*  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 FSetInterface.
+Require FSetBridge.
+Require FSetProperties.
+Require FSetList.
+Require FSetRBT.
+
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
new file mode 100644
index 0000000000..257aa9e8bf
--- /dev/null
+++ b/theories/FSets/FSetBridge.v
@@ -0,0 +1,720 @@
+(***********************************************************************)
+(*  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$ *)
+
+(** This module implements bridges (as functors) from dependent
+    to/from non-dependent set signature. *)
+
+Require Export FSetInterface.
+Set Implicit Arguments.
+
+(** * From non-dependent signature [S] to dependent signature [Sdep]. *)
+
+Module DepOfNodep [M:S] <: Sdep with Module E := M.E.
+  Import M.
+
+  Module ME := MoreOrderedType E.
+   
+  Definition empty: { s:t | Empty s }.
+  Proof. 
+    Exists empty; Auto.
+  Save.
+
+  Definition is_empty: (s:t){ Empty s }+{ ~(Empty s) }.
+  Proof. 
+    Intros; Generalize (!is_empty_1 s) (!is_empty_2 s).
+    Case (is_empty s); Intuition.
+  Save.
+
+
+  Definition mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }.
+  Proof. 
+    Intros; Generalize (!mem_1 s x) (!mem_2 s x).
+    Case (mem x s); Intuition.
+  Save.
+ 
+  Definition add : (x:elt) (s:t){ s':t | (Add x s s') }.
+  Proof.
+    Intros; Exists (add x s); Auto.
+    Unfold Add; Intuition.
+    Elim (ME.eq_dec x y); Auto.
+    Intros; Right. 
+    EApply add_3; EAuto.
+    Apply In_1 with x; Auto.
+  Save. 
+ 
+  Definition singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}.
+  Proof. 
+    Intros; Exists (singleton x); Intuition.
+  Save.
+ 
+  Definition remove : (x:elt)(s:t)
+                     { s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}.
+  Proof.
+    Intros; Exists (remove x s); Intuition.
+    Absurd (In x (remove x s)); Auto.
+    Apply In_1 with y; Auto. 
+    Elim (ME.eq_dec x y); Intros; Auto.
+    Absurd (In x (remove x s)); Auto.
+    Apply In_1 with y; Auto. 
+    EAuto.
+  Save.
+
+  Definition union : (s,s':t)
+                    { s'':t | (x:elt)(In x s'') <-> ((In x s)\/(In x s'))}.
+  Proof.
+    Intros; Exists (union s s'); Intuition.
+  Save.    
+
+  Definition inter : (s,s':t)
+                    { s'':t | (x:elt)(In x s'') <-> ((In x s)/\(In x s'))}.
+  Proof. 
+    Intros; Exists (inter s s'); Intuition; EAuto.
+  Save.
+
+  Definition diff : (s,s':t)
+                    { s'':t | (x:elt)(In x s'') <-> ((In x s)/\~(In x s'))}.
+  Proof. 
+    Intros; Exists (diff s s'); Intuition; EAuto. 
+    Absurd (In x s'); EAuto. 
+  Save. 
+ 
+  Definition equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }.
+  Proof. 
+    Intros. 
+    Generalize (!equal_1 s s') (!equal_2 s s').
+    Case (equal s s');Intuition.
+  Save.
+
+  Definition subset : (s,s':t) { Subset s s' } + { ~(Subset s s') }.
+  Proof. 
+    Intros. 
+    Generalize (!subset_1 s s') (!subset_2 s s').
+    Case (subset s s');Intuition.
+  Save.   
+
+  Definition fold :
+   (A:Set)
+   (f:elt->A->A)
+   { fold:t -> A -> A | (s,s':t)(a:A)
+      (eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) 
+      ((Empty s) -> (eqA (fold s a) a)) /\
+      ((compat_op E.eq eqA f)->(transpose eqA f) ->
+         (x:elt) (Add x s s') -> ~(In x s) -> (eqA (fold s' a) (f x (fold s a)))) }.
+  Proof.
+    Intros; Exists (!fold A f); Intros.
+    Split; Intros.
+    Apply fold_1; Auto.
+    Apply (!fold_2 s s' x A eqA); Auto.
+  Save.  
+
+  Definition cardinal :
+    {cardinal : t -> nat | (s,s':t)
+       ((Empty s) -> (cardinal s)=O) /\
+       ((x:elt) (Add x s s') -> ~(In x s) -> 
+	          (cardinal s')=(S (cardinal s))) }.
+  Proof.
+    Intros; Exists cardinal; EAuto.
+  Save.    
+
+  Definition fdec := 
+    [P:elt->Prop; Pdec:(x:elt){P x}+{~(P x)}; x:elt] 
+    if (Pdec x) then [_]true else [_]false. 
+
+  Lemma compat_P_aux : 
+	(P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(compat_P E.eq P) -> 
+        (compat_bool E.eq (fdec Pdec)).
+  Proof.
+    Unfold compat_P compat_bool fdec; Intros.
+    Generalize (E.eq_sym H0); Case (Pdec x); Case (Pdec y); Ground.
+  Qed.
+
+  Hints Resolve compat_P_aux.
+
+  Definition filter : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { s':t | (compat_P E.eq P) -> (x:elt)(In x s') <-> ((In x s)/\(P x)) }.
+  Proof.
+    Intros. 
+    Exists (filter (fdec Pdec) s).
+    Intro H; Assert (compat_bool E.eq (fdec Pdec)); Auto.
+    Intuition.
+    EAuto.
+    Generalize (filter_2 H0 H1).
+    Unfold fdec.
+    Case (Pdec x); Intuition.
+    Inversion H2.
+    Apply filter_3; Auto.
+    Unfold fdec; Simpl.
+    Case (Pdec x); Intuition.
+  Save.
+
+  Definition for_all : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { (compat_P E.eq P) -> (For_all P s) } + 
+     { (compat_P E.eq P) -> ~(For_all P s) }.
+  Proof. 
+    Intros. 
+    Generalize (!for_all_1 s (fdec Pdec)) (!for_all_2 s (fdec Pdec)).
+    Case (for_all (fdec Pdec) s); Unfold For_all; [Left|Right]; Intros.
+    Assert (compat_bool E.eq (fdec Pdec)); Auto.
+    Generalize (H0 H3 (refl_equal ??) ? H2).
+    Unfold fdec. 
+    Case (Pdec x); Intuition.
+    Inversion H4.
+    Intuition.    
+    Absurd false=true; [Auto with bool|Apply H; Auto].
+    Intro.
+    Unfold fdec. 
+    Case (Pdec x); Intuition.
+  Save.
+
+  Definition exists : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { (compat_P E.eq P) -> (Exists P s) } + 
+     { (compat_P E.eq P) -> ~(Exists P s) }.
+  Proof. 
+    Intros. 
+    Generalize (!exists_1 s (fdec Pdec)) (!exists_2 s (fdec Pdec)).
+    Case (exists (fdec Pdec) s); Unfold Exists; [Left|Right]; Intros.
+    Elim H0; Auto; Intros.
+    Exists x; Intuition.
+    Generalize H4.
+    Unfold fdec. 
+    Case (Pdec x); Intuition.
+    Inversion H2.
+    Intuition. 
+    Elim H2; Intros.    
+    Absurd false=true; [Auto with bool|Apply H; Auto].
+    Exists x; Intuition.
+    Unfold fdec. 
+    Case (Pdec x); Intuition.
+  Save.
+
+  Definition partition : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { partition : t*t |
+        let (s1,s2) = partition in
+        (compat_P E.eq P) -> 
+        ((For_all P s1) /\
+         (For_all ([x]~(P x)) s2) /\
+         (x:elt)(In x s)<->((In x s1)\/(In x s2))) }.
+  Proof.
+    Intros.
+    Exists (partition (fdec Pdec) s).
+    Generalize (!partition_1 s (fdec Pdec)) (!partition_2 s (fdec Pdec)).
+    Case (partition (fdec Pdec) s).
+    Intros s1 s2; Simpl.
+    Intros; Assert (compat_bool E.eq (fdec Pdec)); Auto.
+    Intros; Assert (compat_bool E.eq [x](negb (fdec Pdec x))).
+    Generalize H2; Unfold compat_bool;Intuition; Apply (f_equal ?? negb); Auto.
+    Intuition.
+    Generalize H4; Unfold For_all Equal; Intuition.
+    Elim (H0 x); Intros.
+    Assert (fdec Pdec x)=true.
+     EAuto.      
+    Generalize H8; Unfold fdec; Case (Pdec x); Intuition.
+    Inversion H9.
+    Generalize H; Unfold For_all Equal; Intuition.
+    Elim (H0 x); Intros.
+    Cut ([x](negb (fdec Pdec x)) x)=true. 
+    Unfold fdec; Case (Pdec x); Intuition.
+      Change ([x](negb (fdec Pdec x)) x)=true.
+      Apply (!filter_2 s x); Auto.
+    LetTac b := (fdec Pdec x); Generalize (refl_equal ? b); 
+      Pattern -1 b; Case b; Unfold b; [Left|Right].
+    Elim (H4 x); Intros _ B; Apply B; Auto.
+    Elim (H x); Intros _ B; Apply B; Auto.
+    Apply filter_3; Auto.
+    Rewrite H5; Auto.
+    EApply (filter_1 1!s 2!x H2); Elim (H4 x); Intros B _; Apply B; Auto.
+    EApply (filter_1 1!s 2!x H3); Elim (H x); Intros B _; Apply B; Auto.
+  Save. 
+
+  Definition choose : (s:t) {x:elt | (In x s)} + { Empty s }.
+  Proof.  
+    Intros.
+    Generalize (!choose_1 s) (!choose_2 s).
+    Case (choose s); [Left|Right]; Auto.
+    Exists e; Auto.    
+  Save.
+
+  Definition elements : 
+     (s:t){ l:(list elt) | (sort E.lt l)/\(x:elt)(In x s)<->(InList E.eq x l)}.
+   Proof.
+     Intros; Exists (elements s); Intuition.   
+   Save. 
+
+  Definition min_elt : 
+    (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }.
+  Proof. 
+    Intros; Generalize (!min_elt_1 s) (!min_elt_2 s) (!min_elt_3 s).
+    Case (min_elt s); [Left|Right]; Auto.    
+    Exists e; Unfold For_all; EAuto.
+  Save. 
+
+  Definition max_elt : 
+    (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }.
+  Proof. 
+    Intros; Generalize (!max_elt_1 s) (!max_elt_2 s) (!max_elt_3 s).
+    Case (max_elt s); [Left|Right]; Auto.    
+    Exists e; Unfold For_all; EAuto.
+  Save. 
+
+  Module E:=E. 
+
+  Definition elt := elt.
+  Definition t := t.
+
+  Definition In := In. 
+  Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
+  Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
+  Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
+  Definition Empty := [s](a:elt)~(In a s).
+  Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
+  Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
+  
+  Definition eq_In := In_1.
+
+  Definition eq := eq.
+  Definition lt := lt.
+  Definition eq_refl := eq_refl.
+  Definition eq_sym := eq_sym.
+  Definition eq_trans := eq_trans.
+  Definition lt_trans := lt_trans. 
+  Definition lt_not_eq := lt_not_eq.
+  Definition compare := compare.
+
+End DepOfNodep.
+
+
+(** * From dependent signature [Sdep] to non-dependent signature [S]. *)
+
+Module NodepOfDep [M:Sdep] <: S with Module E := M.E.
+  Import M.
+
+  Module ME := MoreOrderedType E.
+
+  Definition empty : t := let (s,_) = M.empty in s.
+
+  Lemma empty_1 : (Empty empty).
+  Proof.
+    Unfold empty; Case M.empty; Auto.
+  Save.
+
+  Definition is_empty : t -> bool := 
+    [s:t]if (M.is_empty s) then [_]true else [_]false.
+
+  Lemma is_empty_1 : (s:t)(Empty s) -> (is_empty s)=true.
+  Proof.
+    Intros; Unfold is_empty; Case (M.is_empty s); Auto.
+  Save.
+
+  Lemma is_empty_2 : (s:t)(is_empty s)=true -> (Empty s).
+  Proof.
+    Intro s; Unfold is_empty; Case (M.is_empty s); Auto.
+    Intros; Discriminate H.
+  Save.
+
+  Definition mem : elt -> t -> bool := 
+    [x:elt][s:t]if (M.mem x s) then [_]true else [_]false.
+
+  Lemma mem_1 : (s:t)(x:elt)(In x s) -> (mem x s)=true.
+  Proof.
+    Intros; Unfold mem; Case (M.mem x s); Auto.
+  Save.
+   
+  Lemma mem_2 : (s:t)(x:elt)(mem x s)=true -> (In x s).
+  Proof.
+    Intros s x; Unfold mem; Case (M.mem x s); Auto.
+    Intros; Discriminate H.
+  Save.
+
+  Definition equal : t -> t -> bool := 
+    [s,s']if (M.equal s s') then [_]true else [_]false.
+
+  Lemma equal_1 : (s,s':t)(Equal s s') -> (equal s s')=true.
+  Proof. 
+    Intros; Unfold equal; Case M.equal; Intuition.
+  Save.    
+ 
+  Lemma equal_2 : (s,s':t)(equal s s')=true -> (Equal s s').
+  Proof. 
+    Intros s s'; Unfold equal; Case (M.equal s s'); Intuition; Inversion H.
+  Save.
+  
+  Definition subset : t -> t -> bool := 
+    [s,s']if (M.subset s s') then [_]true else [_]false.
+
+  Lemma subset_1 : (s,s':t)(Subset s s') -> (subset s s')=true.
+  Proof. 
+    Intros; Unfold subset; Case M.subset; Intuition.
+  Save.    
+ 
+  Lemma subset_2 : (s,s':t)(subset s s')=true -> (Subset s s').
+  Proof. 
+    Intros s s'; Unfold subset; Case (M.subset s s'); Intuition; Inversion H.
+  Save.
+
+  Definition choose : t -> (option elt) :=
+    [s:t]Cases (M.choose s) of (inleft (exist x _)) => (Some ? x)
+                             | (inright _) => (None ?) end.
+
+  Lemma choose_1 : (s:t)(x:elt) (choose s)=(Some ? x) -> (In x s).
+  Proof.
+    Intros s x; Unfold choose; Case (M.choose s).
+    Destruct s0; Intros; Injection H; Intros; Subst; Auto.
+    Intros; Discriminate H.
+  Save.
+
+  Lemma choose_2 : (s:t)(choose s)=(None ?) -> (Empty s).
+  Proof.
+    Intro s; Unfold choose; Case (M.choose s); Auto.
+    Destruct s0; Intros; Discriminate H.
+  Save.
+
+  Definition elements : t -> (list elt) := [s] let (l,_) = (M.elements s) in l. 
+ 
+  Lemma elements_1: (s:t)(x:elt)(In x s) -> (InList E.eq x (elements s)).
+  Proof. 
+    Intros; Unfold elements; Case (M.elements s); Ground.
+  Save.
+
+  Lemma elements_2: (s:t)(x:elt)(InList E.eq x (elements s)) -> (In x s).
+  Proof. 
+    Intros s x; Unfold elements; Case (M.elements s); Ground.
+  Save.
+
+  Lemma elements_3: (s:t)(sort E.lt (elements s)).  
+  Proof. 
+    Intros; Unfold elements; Case (M.elements s); Ground.
+  Save.
+
+  Definition min_elt : t -> (option elt) :=
+    [s:t]Cases (M.min_elt s) of (inleft (exist x _)) => (Some ? x)
+                             | (inright _) => (None ?) end.
+
+  Lemma min_elt_1: (s:t)(x:elt)(min_elt s) = (Some ? x) -> (In x s). 
+  Proof.
+    Intros s x; Unfold min_elt; Case (M.min_elt s).
+    Destruct s0; Intros; Injection H; Intros; Subst; Intuition.
+    Intros; Discriminate H.
+  Save. 
+
+  Lemma min_elt_2: (s:t)(x,y:elt)(min_elt s) = (Some ? x) -> (In y s) -> ~(E.lt y x). 
+  Proof.
+    Intros s x y; Unfold min_elt; Case (M.min_elt s).
+    Unfold For_all; Destruct s0; Intros; Injection H; Intros; Subst; Ground.
+    Intros; Discriminate H.
+  Save. 
+
+  Lemma min_elt_3 : (s:t)(min_elt s) = (None ?) -> (Empty s).
+  Proof.
+    Intros s; Unfold min_elt; Case (M.min_elt s); Auto.
+    Destruct s0; Intros; Discriminate H.
+  Save. 
+
+  Definition max_elt : t -> (option elt) :=
+    [s:t]Cases (M.max_elt s) of (inleft (exist x _)) => (Some ? x)
+                             | (inright _) => (None ?) end.
+
+  Lemma max_elt_1: (s:t)(x:elt)(max_elt s) = (Some ? x) -> (In x s). 
+  Proof.
+    Intros s x; Unfold max_elt; Case (M.max_elt s).
+    Destruct s0; Intros; Injection H; Intros; Subst; Intuition.
+    Intros; Discriminate H.
+  Save. 
+
+  Lemma max_elt_2: (s:t)(x,y:elt)(max_elt s) = (Some ? x) -> (In y s) -> ~(E.lt x y). 
+  Proof.
+    Intros s x y; Unfold max_elt; Case (M.max_elt s).
+    Unfold For_all; Destruct s0; Intros; Injection H; Intros; Subst; Ground.
+    Intros; Discriminate H.
+  Save. 
+
+  Lemma max_elt_3 : (s:t)(max_elt s) = (None ?) -> (Empty s).
+  Proof.
+    Intros s; Unfold max_elt; Case (M.max_elt s); Auto.
+    Destruct s0; Intros; Discriminate H.
+  Save. 
+
+  Definition add : elt -> t -> t := 
+    [x:elt][s:t]let (s',_) = (M.add x s) in s'.
+
+  Lemma add_1 : (s:t)(x:elt)(In x (add x s)).
+  Proof.
+    Intros; Unfold add; Case (M.add x s); Unfold Add; Ground.
+  Save.
+
+  Lemma add_2 : (s:t)(x,y:elt)(In y s) -> (In y (add x s)).
+  Proof.
+    Intros; Unfold add; Case (M.add x s); Unfold Add; Ground.
+  Save.
+
+  Lemma add_3 : (s:t)(x,y:elt)~(E.eq x y) -> (In y (add x s)) -> (In y s).
+  Proof.
+    Intros s x y; Unfold add; Case (M.add x s); Unfold Add; Ground.
+    Generalize (a y); Intuition; Absurd (E.eq x y); Auto.
+  Save.
+
+  Definition remove : elt -> t -> t := 
+    [x:elt][s:t]let (s',_) = (M.remove x s) in s'.
+
+  Lemma remove_1 : (s:t)(x:elt)~(In x (remove x s)).
+  Proof.
+    Intros; Unfold remove; Case (M.remove x s); Ground.
+  Save.
+
+  Lemma remove_2 : (s:t)(x,y:elt)
+	~(E.eq x y) ->(In y s) -> (In y (remove x s)).
+  Proof.
+    Intros; Unfold remove; Case (M.remove x s); Ground.
+  Save.
+
+  Lemma remove_3 : (s:t)(x,y:elt)(In y (remove x s)) -> (In y s).
+  Proof.
+    Intros s x y; Unfold remove; Case (M.remove x s); Ground.
+  Save.
+  
+  Definition singleton : elt -> t := [x]let (s,_) = (M.singleton x) in s. 
+ 
+  Lemma singleton_1 : (x,y:elt)(In y (singleton x)) -> (E.eq x y). 
+  Proof.
+    Intros x y; Unfold singleton; Case (M.singleton x); Ground.
+  Save.
+
+  Lemma singleton_2: (x,y:elt)(E.eq x y) -> (In y (singleton x)). 
+  Proof.
+    Intros x y; Unfold singleton; Case (M.singleton x); Ground.
+  Save.
+  
+  Definition union : t -> t -> t := 
+	[s,s']let (s'',_) = (M.union s s') in s''.
+ 
+  Lemma union_1: (s,s':t)(x:elt)(In x (union s s')) -> (In x s)\/(In x s').
+  Proof. 
+    Intros s s' x; Unfold union; Case (M.union s s'); Ground.
+  Save.
+
+  Lemma union_2: (s,s':t)(x:elt)(In x s) -> (In x (union s s')). 
+  Proof. 
+    Intros s s' x; Unfold union; Case (M.union s s'); Ground.
+  Save.
+
+  Lemma union_3: (s,s':t)(x:elt)(In x s') ->  (In x (union s s')).
+  Proof. 
+    Intros s s' x; Unfold union; Case (M.union s s'); Ground.
+  Save.
+
+  Definition inter : t -> t -> t := 
+	[s,s']let (s'',_) = (M.inter s s') in s''.
+ 
+  Lemma inter_1: (s,s':t)(x:elt)(In x (inter s s')) -> (In x s).
+  Proof. 
+    Intros s s' x; Unfold inter; Case (M.inter s s'); Ground.
+  Save.
+
+  Lemma inter_2: (s,s':t)(x:elt)(In x (inter s s')) -> (In x s').
+  Proof. 
+    Intros s s' x; Unfold inter; Case (M.inter s s'); Ground.
+  Save.
+
+  Lemma inter_3: (s,s':t)(x:elt)(In x s) -> (In x s') -> (In x (inter s s')).
+  Proof. 
+    Intros s s' x; Unfold inter; Case (M.inter s s'); Ground.
+  Save.
+
+  Definition diff : t -> t -> t := 
+	[s,s']let (s'',_) = (M.diff s s') in s''.
+ 
+  Lemma diff_1: (s,s':t)(x:elt)(In x (diff s s')) -> (In x s).
+  Proof. 
+    Intros s s' x; Unfold diff; Case (M.diff s s'); Ground.
+  Save.
+
+  Lemma diff_2: (s,s':t)(x:elt)(In x (diff s s')) -> ~(In x s').
+  Proof. 
+    Intros s s' x; Unfold diff; Case (M.diff s s'); Ground.
+  Save.
+
+  Lemma diff_3: (s,s':t)(x:elt)(In x s) -> ~(In x s') -> (In x (diff s s')).
+  Proof. 
+    Intros s s' x; Unfold diff; Case (M.diff s s'); Ground.
+  Save.
+
+  Definition cardinal : t -> nat := let (f,_)= M.cardinal in f.
+
+  Lemma cardinal_1 : (s:t)(Empty s) -> (cardinal s)=O.
+  Proof. 
+    Intros; Unfold cardinal; Case M.cardinal; Ground.
+  Qed.
+
+  Lemma cardinal_2 : 
+    (s,s':t)(x:elt)~(In x s) -> (Add x s s') -> 
+	(cardinal s')=(S (cardinal s)).
+  Proof. 
+    Intros; Unfold cardinal; Case M.cardinal; Ground.
+  Qed.
+
+  Definition fold : (B:Set)(elt->B->B)->t->B->B :=  
+       [B,f]let (fold,_)= (M.fold f) in fold.
+
+  Lemma fold_1: 
+    (s:t)(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.
+    Intros; Unfold fold; Case (M.fold f); Ground.
+  Save.  
+
+  Lemma fold_2:
+    (s,s':t)(x:elt)(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; Unfold fold; Case (M.fold f); Ground.
+  Save.
+
+  Definition f_dec : 
+    (f: elt -> bool)(x:elt){ (f x)=true } + { (f x)<>true }.
+  Proof.
+    Intros; Case (f x); Auto with bool.
+  Defined. 
+
+  Lemma compat_P_aux : 
+     (f:elt -> bool)(compat_bool E.eq f) -> (compat_P E.eq [x](f x)=true).
+  Proof.
+     Unfold compat_bool compat_P; Intros; Rewrite <- H1; Ground.
+  Qed.
+
+  Hints Resolve compat_P_aux.
+    
+  Definition filter : (elt -> bool) -> t -> t := 
+     [f,s]let (s',_) = (!M.filter [x](f x)=true (f_dec f) s) in s'.
+
+  Lemma filter_1: (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) -> 
+     (In x (filter f s)) -> (In x s).
+  Proof.
+    Intros s x f; Unfold filter; Case M.filter; Intuition.
+    Generalize (i (compat_P_aux H)); Ground.
+  Save.
+
+  Lemma filter_2: 
+    (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->(In x (filter f s)) -> (f x)=true. 
+  Proof.
+    Intros s x f; Unfold filter; Case M.filter; Intuition.
+    Generalize (i (compat_P_aux H)); Ground.
+  Save.
+
+  Lemma filter_3: 
+    (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) -> 
+        (In x s) -> (f x)=true -> (In x (filter f s)).     
+  Proof.
+    Intros s x f; Unfold filter; Case M.filter; Intuition.
+    Generalize (i (compat_P_aux H)); Ground.
+  Save.
+
+  Definition for_all: (elt -> bool) -> t -> bool := 
+     [f,s]if (!M.for_all [x](f x)=true (f_dec f) s) then [_]true else [_]false. 
+
+  Lemma for_all_1: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> 
+       (For_all [x](f x)=true s) -> (for_all f s)=true.
+  Proof. 
+    Intros s f; Unfold for_all; Case M.for_all; Intuition; Elim n; Auto.
+  Qed.
+ 
+  Lemma for_all_2: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) ->(for_all f s)=true -> (For_all [x](f x)=true s).
+  Proof. 
+    Intros s f; Unfold for_all; Case M.for_all; Intuition; Inversion H0.
+  Qed.
+  
+  Definition exists: (elt -> bool) -> t -> bool := 
+     [f,s]if (!M.exists [x](f x)=true (f_dec f) s) then [_]true else [_]false. 
+
+  Lemma exists_1: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) ->
+       (Exists [x](f x)=true s) -> (exists f s)=true.
+  Proof. 
+    Intros s f; Unfold exists; Case M.exists; Intuition; Elim n; Auto.
+  Qed.
+ 
+  Lemma exists_2: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> 
+       (exists f s)=true -> (Exists [x](f x)=true s).
+  Proof. 
+    Intros s f; Unfold exists; Case M.exists; Intuition; Inversion H0.
+  Qed.
+     
+  Definition partition : (elt -> bool) -> t -> t*t := 
+    [f,s]let (p,_) = (!M.partition [x](f x)=true (f_dec f) s) in p.
+  
+  Lemma partition_1: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> (Equal (fst ? ? (partition f s)) (filter f s)).
+  Proof.
+    Intros s f; Unfold partition; Case M.partition. 
+    Intro p; Case p; Clear p; Intros s1 s2 H C. 
+    Generalize (H (compat_P_aux C)); Clear H; Intro H.
+    Simpl; Unfold Equal; Intuition.
+    Apply filter_3; Ground. 
+    Apply (H0 a); Auto.
+    Elim (H2 a); Intros. 
+    Assert (In a s). 
+     EApply filter_1; EAuto.
+    Elim H3; Intros; Auto.
+    Absurd (f a)=true.
+    Exact (H a H6).
+    EApply filter_2; EAuto. 
+  Qed.    
+    
+  Lemma partition_2: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> 
+    (Equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s)).
+  Proof.
+    Intros s f; Unfold partition; Case M.partition. 
+    Intro p; Case p; Clear p; Intros s1 s2 H C. 
+    Generalize (H (compat_P_aux C)); Clear H; Intro H.
+    Assert D: (compat_bool E.eq [x](negb (f x))).
+    Generalize C; Unfold compat_bool; Intros; Apply (f_equal ?? negb); Auto.
+    Simpl; Unfold Equal; Intuition.
+    Apply filter_3; Ground.
+    Generalize (H a H1); Case (f a); Intuition.
+    Elim (H2 a); Intros. 
+    Assert (In a s). 
+     EApply filter_1; EAuto.
+    Elim H3; Intros; Auto.
+    Absurd (f a)=true.
+    Intro.
+    Generalize (filter_2  D H1). 
+    Rewrite H7; Intros H8; Inversion H8.
+    Exact (H0 a H6).
+  Qed. 
+
+
+  Module E:=E. 
+  Definition elt := elt.
+  Definition t := t.
+
+  Definition In := In. 
+  Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
+  Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
+  Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
+  Definition Empty := [s](a:elt)~(In a s).
+  Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
+  Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
+
+  Definition In_1 := eq_In.
+
+  Definition eq := eq.
+  Definition lt := lt.
+  Definition eq_refl := eq_refl.
+  Definition eq_sym := eq_sym.
+  Definition eq_trans := eq_trans.
+  Definition lt_trans := lt_trans. 
+  Definition lt_not_eq := lt_not_eq.
+  Definition compare := compare.
+
+End NodepOfDep.
+
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
new file mode 100644
index 0000000000..ddd12838d6
--- /dev/null
+++ b/theories/FSets/FSetInterface.v
@@ -0,0 +1,643 @@
+(***********************************************************************)
+(*  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$ *)
+
+(** Set interfaces *)
+
+Require Export Bool.
+Require Export PolyList.
+Require Export Sorting.
+Require Export Setoid.
+Set Implicit Arguments.
+
+(** Misc properties used in specifications. *)
+
+Section Misc.
+Variable A,B : Set.
+Variable eqA : A -> A -> Prop. 
+Variable eqB : B -> B -> Prop.
+
+(** Two-argument functions that allow to reorder its arguments. *)
+Definition transpose := [f:A->B->B](x,y:A)(z:B)(eqB (f x (f y z)) (f y (f x z))). 
+
+(** Compatibility of a  boolean function with respect to an equality. *)
+Definition compat_bool := [f:A->bool] (x,y:A)(eqA x y) -> (f x)=(f y).
+
+(** Compatibility of a two-argument function with respect to two equalities. *)
+Definition compat_op := [f:A->B->B](x,x':A)(y,y':B)(eqA x x') -> (eqB y y') -> 
+ (eqB (f x y) (f x' y')).
+
+(** Compatibility of a predicate with respect to an equality. *)
+Definition compat_P := [P:A->Prop](x,y:A)(eqA x y) -> (P x) -> (P y).
+
+(** Being in a list modulo an equality relation. *)
+Inductive InList [x:A] : (list A) -> Prop :=
+  | InList_cons_hd : (y:A)(l:(list A))(eqA x y) -> (InList x (cons y l))
+  | InList_cons_tl : (y:A)(l:(list A))(InList x l) -> (InList x (cons y l)).
+
+End Misc.
+
+Hint InList := Constructors InList.
+Hint sort := Constructors sort.
+Hint lelistA := Constructors lelistA.
+Hints Unfold transpose compat_bool compat_op compat_P.
+
+(** * Ordered types *)
+
+Inductive Compare [X:Set; lt,eq:X->X->Prop; x,y:X] : Set :=
+  | Lt : (lt x y) -> (Compare lt eq x y)
+  | Eq : (eq x y) -> (Compare lt eq x y)
+  | Gt : (lt y x) -> (Compare lt eq x y).
+
+Module Type OrderedType.
+
+  Parameter t : Set.
+
+  Parameter eq : t -> t -> Prop.
+  Parameter lt : t -> t -> Prop.
+
+  Axiom eq_refl : (x:t) (eq x x).
+  Axiom eq_sym : (x,y:t) (eq x y) -> (eq y x).
+  Axiom eq_trans : (x,y,z:t) (eq x y) -> (eq y z) -> (eq x z).
+ 
+  Axiom lt_trans : (x,y,z:t) (lt x y) -> (lt y z) -> (lt x z).
+  Axiom lt_not_eq : (x,y:t) (lt x y) -> ~(eq x y).
+
+  Parameter compare : (x,y:t)(Compare lt eq x y).
+
+  Hints Immediate eq_sym.
+  Hints Resolve eq_refl eq_trans lt_not_eq lt_trans.
+
+End OrderedType.
+
+(** * Non-dependent signature
+
+    Signature [S] presents sets as purely informative programs 
+    together with axioms *)
+
+Module Type S.
+
+  Declare Module E : OrderedType.
+  Definition elt := E.t.
+
+  Parameter t : Set. (** the abstract type of sets *)
+ 
+  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. *)
+
+  Parameter eq : t -> t -> Prop.
+  Parameter lt : t -> t -> Prop.
+  Parameter compare: (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 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:  (A:Set)(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.
+  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 *)
+
+  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. *)
+  (** Coq comment: [Not_found] is represented by the option type *)
+  (** Coq comment: We do not necessary choose equal elements from 
+     equal sets. *)
+
+  Section Spec. 
+
+  Variable s,s',s'' : t.
+  Variable x,y,z : elt.
+
+  Parameter In : elt -> t -> Prop.
+  Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
+  Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
+  Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
+  Definition Empty := [s](a:elt)~(In a s).
+  Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
+  Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
+
+  (** 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: (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: (In x (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: ~(In x (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: 
+   (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).
+   
+  Parameter fold_2: 
+    (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))).
+
+  (** Specification of [cardinal] *)  
+  Parameter cardinal_1: (Empty s) -> (cardinal s)=O.
+  Parameter cardinal_2:  
+    ~(In x s) -> (Add x s s') -> (cardinal s')=(S (cardinal 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 [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 [x](f x)=true s).
+
+  (** Specification of [exists] *)
+  Parameter exists_1: 
+    (compat_bool E.eq f) -> (Exists [x](f x)=true s) -> (exists f s)=true.
+  Parameter exists_2: 
+    (compat_bool E.eq f) -> (exists f s)=true -> (Exists [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 [x](negb (f x)) s)).
+
+  (** Specification of [elements] *)
+  Parameter elements_1: (In x s) -> (InList E.eq x (elements s)).
+  Parameter elements_2: (InList E.eq x (elements s)) -> (In x s).
+  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). 
+  Parameter min_elt_3: (min_elt s) = (None ?) -> (Empty s).
+
+  (** Specification of [max_elt] *)  
+  Parameter max_elt_1: (max_elt s) = (Some ? x) -> (In x 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).
+  (*i Parameter choose_equal: 
+      (equal s s')=true -> (compare (choose s) (choose s'))=E. i*)
+
+  End Filter.
+  End Spec.
+
+  Notation "∅" := empty.
+  Notation "a ⋃ b" := (union a b) (at level 1).
+  Notation "a ⋂ b" := (inter a b) (at level 1). 
+  Notation "∥ a ∥" := (cardinal a) (at level 1).
+  Notation "a ∈ b" := (In a b) (at level 1).
+  Notation "a ∉ b" := ~(In a b) (at level 1).
+  Notation "a ≡ b" := (Equal a b) (at level 1).
+  Notation "a ≢ b" := ~(Equal a b) (at level 1).
+  Notation "a ⊆ b" := (Subset a b) (at level 1).
+  Notation "a ⊈ b" := ~(Subset a b) (at level 1).  
+
+  Hints Immediate 
+  In_1.
+  
+  Hints Resolve 
+  mem_1 mem_2
+  equal_1 equal_2
+  subset_1 subset_2
+  empty_1
+  is_empty_1 is_empty_2
+  choose_1
+  choose_2
+  add_1 add_2 add_3
+  remove_1 remove_2 remove_3
+  singleton_1 singleton_2
+  union_1 union_2 union_3
+  inter_1 inter_2 inter_3 
+  diff_1 diff_2 diff_3
+  cardinal_1 cardinal_2
+  filter_1 filter_2 filter_3
+  for_all_1 for_all_2
+  exists_1 exists_2
+  partition_1 partition_2
+  elements_1 elements_2 elements_3
+  min_elt_1 min_elt_2 min_elt_3
+  max_elt_1 max_elt_2 max_elt_3.
+
+End S.
+
+(** * Dependent signature 
+
+    Signature [Sdep] presents sets using dependent types *)
+
+Module Type Sdep.
+
+  Declare Module E : OrderedType.
+  Definition elt := E.t.
+
+  Parameter t : Set.
+
+  Parameter eq : t -> t -> Prop.
+  Parameter lt : t -> t -> Prop.
+  Parameter compare: (s,s':t)(Compare lt eq s s').
+
+  Parameter eq_refl: (s:t)(eq s s). 
+  Parameter eq_sym: (s,s':t)(eq s s') -> (eq s' s).
+  Parameter eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s'').
+  Parameter lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s'').
+  Parameter lt_not_eq : (s,s':t)(lt s s') -> ~(eq s s').
+
+  Parameter In : elt -> t -> Prop.
+  Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
+  Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
+  Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
+  Definition Empty := [s](a:elt)~(In a s).
+  Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
+  Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
+
+  Parameter eq_In: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s).
+
+  Parameter empty : { s:t | Empty s }.
+
+  Parameter is_empty : (s:t){ Empty s }+{ ~(Empty s) }.
+
+  Parameter mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }.
+
+  Parameter add : (x:elt) (s:t) { s':t | (Add x s s') }.
+
+  Parameter singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}.
+  
+  Parameter remove : (x:elt)(s:t)
+                     { s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}.
+
+  Parameter union : (s,s':t)
+                    { s'':t | (x:elt)(In x s'') <-> ((In x s)\/(In x s'))}.
+
+  Parameter inter : (s,s':t)
+                    { s'':t | (x:elt)(In x s'') <-> ((In x s)/\(In x s'))}.
+
+  Parameter diff : (s,s':t)
+                    { s'':t | (x:elt)(In x s'') <-> ((In x s)/\~(In x s'))}.
+
+  Parameter equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }.
+ 
+  Parameter subset : (s,s':t) { Subset s s' } + { ~(Subset s s') }.
+
+  Parameter fold : 
+   (A:Set)
+   (f:elt->A->A) 
+   { fold:t -> A -> A | (s,s':t)(a:A)
+      (eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
+      ((Empty s) -> (eqA (fold s a) a)) /\
+      ((compat_op E.eq eqA f)->(transpose eqA f) ->
+        (x:elt) (Add x s s') -> ~(In x s) -> (eqA (fold s' a) (f x (fold s a)))) }.  
+
+  Parameter cardinal : 
+    {cardinal : t -> nat | (s,s':t)
+       ((Empty s) -> (cardinal s)=O) /\
+       ((x:elt) (Add x s s') -> ~(In x s) -> (cardinal s')=(S (cardinal s)))}.
+
+  Parameter filter : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { s':t | (compat_P E.eq P) -> (x:elt)(In x s') <-> ((In x s)/\(P x)) }.
+
+  Parameter for_all : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { (compat_P E.eq P) -> (For_all P s) } + 
+     { (compat_P E.eq P) -> ~(For_all P s) }.
+  
+  Parameter exists : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { (compat_P E.eq P) -> (Exists P s) } + 
+     { (compat_P E.eq P) -> ~(Exists P s) }.
+
+  Parameter partition : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { partition : t*t | 
+        let (s1,s2) = partition in 
+	(compat_P E.eq P) -> 
+	((For_all P s1) /\ 
+	 (For_all ([x]~(P x)) s2) /\
+	 (x:elt)(In x s)<->((In x s1)\/(In x s2))) }.
+
+  Parameter elements : 
+     (s:t){ l:(list elt) | (sort E.lt l) /\ (x:elt)(In x s)<->(InList E.eq x l)}.
+
+  Parameter min_elt : 
+     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }.
+
+  Parameter max_elt : 
+     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }.
+
+  Parameter choose : (s:t) { x:elt | (In x s)} + { Empty s }.
+
+  Notation "∅" := empty.
+  Notation "a ⋃ b" := (union a b) (at level 1).
+  Notation "a ⋂ b" := (inter a b) (at level 1).
+  Notation "a ∈ b" := (In a b) (at level 1).
+  Notation "a ∉ b" := ~(In a b) (at level 1).
+  Notation "a ≡ b" := (Equal a b) (at level 1).
+  Notation "a ≢ b" := ~(Equal a b) (at level 1).
+  Notation "a ⊆ b" := (Subset a b) (at level 1).
+  Notation "a ⊈ b" := ~(Subset a b) (at level 1).  
+	
+End Sdep.
+
+(** * Ordered types properties *)
+
+(** Additional properties that can be derived from signature
+    [OrderedType]. *)
+
+Module MoreOrderedType [O:OrderedType]. 
+
+  Lemma gt_not_eq : (x,y:O.t)(O.lt y x) -> ~(O.eq x y).
+  Proof.
+   Intros; Intro; Absurd (O.eq y x); Auto.
+  Qed.	
+ 
+  Lemma eq_not_lt : (x,y:O.t)(O.eq x y) -> ~(O.lt x y).
+  Proof. 
+   Intros; Intro; Absurd (O.eq x y); Auto.
+  Qed.
+
+  Hints Resolve gt_not_eq eq_not_lt.
+
+  Lemma eq_not_gt : (x,y:O.t)(O.eq x y) -> ~(O.lt y x).
+  Proof. 
+   Auto. 
+  Qed.
+  
+  Lemma lt_antirefl : (x:O.t)~(O.lt x x).
+  Proof.
+   Intros; Intro; Absurd (O.eq x x); Auto. 
+  Qed.
+
+  Lemma lt_not_gt : (x,y:O.t)(O.lt x y) -> ~(O.lt y x).
+  Proof. 
+   Intros; Intro; Absurd (O.eq x x); EAuto.
+  Qed.
+
+  Hints Resolve eq_not_gt lt_antirefl lt_not_gt.
+
+  Lemma lt_eq : (x,y,z:O.t)(O.lt x y) -> (O.eq y z) -> (O.lt x z).
+  Proof. 
+   Intros; Case (O.compare x z); Intros; Auto.
+   Absurd (O.eq x y); EAuto.
+   Absurd (O.eq z y); EAuto. 
+  Qed. 
+ 
+  Lemma eq_lt : (x,y,z:O.t)(O.eq x y) -> (O.lt y z) -> (O.lt x z).    
+  Proof.
+    Intros; Case (O.compare x z); Intros; Auto.
+   Absurd (O.eq y z); EAuto.
+   Absurd (O.eq x y); EAuto. 
+  Qed. 
+
+  Hints Immediate eq_lt lt_eq.
+
+  Lemma elim_compare_eq: 
+   (x,y:O.t) (O.eq x y) -> 
+      (EX H : (O.eq x y) | (O.compare x y) = (Eq ? H)).
+  Proof. 
+   Intros; Case (O.compare x y); Intros H'.
+   Absurd (O.eq x y); Auto. 
+   Exists H'; Auto.   
+   Absurd (O.eq x y); Auto.
+  Qed.
+
+  Lemma elim_compare_lt: 
+   (x,y:O.t) (O.lt x y) -> 
+      (EX H : (O.lt x y) | (O.compare x y) = (Lt ? H)).
+  Proof. 
+   Intros; Case (O.compare x y); Intros H'.
+   Exists H'; Auto.   
+   Absurd (O.eq x y); Auto. 
+   Absurd (O.lt x x); EAuto.
+  Qed.
+
+  Lemma elim_compare_gt: 
+   (x,y:O.t) (O.lt y x) -> 
+      (EX H : (O.lt y x) | (O.compare x y) = (Gt ? H)).
+  Proof. 
+   Intros; Case (O.compare x y); Intros H'.
+   Absurd (O.lt x x); EAuto.
+   Absurd (O.eq x y); Auto.
+   Exists H'; Auto.   
+  Qed.
+
+  Tactic Definition Comp_eq x y := 
+    Elim (!elim_compare_eq x y); 
+    [Intros _1 _2; Rewrite _2; Clear _1 _2 | Auto]. 
+
+  Tactic Definition Comp_lt x y := 
+    Elim (!elim_compare_lt x y); 
+    [Intros _1 _2; Rewrite _2; Clear _1 _2 | Auto]. 
+
+  Tactic Definition Comp_gt x y := 
+    Elim (!elim_compare_gt x y); 
+    [Intros _1 _2; Rewrite _2; Clear _1 _2 | Auto].
+
+  Lemma eq_dec : (x,y:O.t){(O.eq x y)}+{~(O.eq x y)}.
+  Proof.
+   Intros; Elim (O.compare x y);[Right|Left|Right];Auto.
+  Qed.
+ 
+  Lemma lt_dec : (x,y:O.t){(O.lt x y)}+{~(O.lt x y)}.
+  Proof.
+   Intros; Elim (O.compare x y);[Left|Right|Right];Auto.
+  Qed.
+
+  (** Results concerning lists modulo E.eq *)
+  
+  Notation "'Sort' l" := (sort O.lt l) (at level 10, l at level 8).
+  Notation "'Inf' x l" := (lelistA O.lt x l) (at level 10, x,l at level 8).
+  Notation "'In' x l" := (InList O.eq x l) (at level 10, x,l at level 8).
+
+  Lemma In_eq: (s:(list O.t))(x,y:O.t)(O.eq x y) -> (In x s) -> (In y s).
+  Proof. 
+   Intros; Elim H0; Intuition; EAuto.
+  Qed.
+  Hints Immediate In_eq.
+  
+  Lemma Inf_lt : (s:(list O.t))(x,y:O.t)(O.lt x y) -> (Inf y s) -> (Inf x s).
+  Proof.
+  Intro s; Case s; Constructor; Inversion H0; EAuto.
+  Qed.
+ 
+  Lemma Inf_eq : (s:(list O.t))(x,y:O.t)(O.eq x y) -> (Inf y s) -> (Inf x s).
+  Proof.
+  Intro s; Case s; Constructor; Inversion H0; EApply eq_lt; EAuto.
+  Qed.
+  Hints Resolve Inf_lt Inf_eq. 
+
+  Lemma In_sort: (s:(list O.t))(x,a:O.t)(Inf a s) -> (In x s) -> (Sort s) -> (O.lt a x).
+  Proof. 
+  Induction s.
+  Intros; Inversion H0.
+  Intros.
+  Inversion_clear H0; Inversion_clear H2; Inversion_clear H1.
+  EApply lt_eq; EAuto.
+  EAuto.
+  Qed.
+  
+  Lemma Inf_In : (l:(list O.t))(x:O.t)
+    ((y:O.t)(PolyList.In y l) -> (O.lt x y)) -> (Inf x l).
+  Proof.
+    Induction l; Simpl; Intros; Constructor; Auto.
+  Save.
+ 
+  Lemma Inf_In_2 : (l:(list O.t))(x:O.t)
+    ((y:O.t)(In y l) -> (O.lt x y)) -> (Inf x l).
+  Proof.
+    Induction l; Simpl; Intros; Constructor; Auto.
+  Save.
+  
+  Lemma In_InList : (l:(list O.t))(x:O.t)(PolyList.In x l) -> (In x l).
+  Proof.
+   Induction l; Simpl; Intuition.
+    Subst; Auto.  
+  Save.
+  Hints Resolve In_InList.
+
+End MoreOrderedType.
+
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
new file mode 100644
index 0000000000..0c8e8287bd
--- /dev/null
+++ b/theories/FSets/FSetList.v
@@ -0,0 +1,1218 @@
+(***********************************************************************)
+(*  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$ *)
+
+(** This file propose an implementation of the AbstractSet non-dependant 
+    interface by strictly ordered list. *)
+
+Require Export FSetInterface.
+
+Set Implicit Arguments.
+
+(* Usual syntax for lists. 
+   CAVEAT: the Coq cast "::" will no longer be available. *)
+Notation "[]" := (nil ?) (at level 1).
+Notation "a :: l" := (cons a l) (at level 1, l at next level).
+
+(** In a first time, we provide sets as lists which are not necessarily sorted.
+   The specs are proved under the additional condition of being sorted. 
+   And the functions outputting sets are proved to preserve this invariant. *)
+
+Module Raw [X : OrderedType].
+ 
+  Module E := X.
+  Module ME := MoreOrderedType X.
+
+  Definition elt := E.t.
+  Definition t := (list elt).
+
+  Definition empty : t := [].
+
+  Definition is_empty : t -> bool := [l]if l then true else [_,_]false.
+
+  (** The set operations. *)
+
+  Fixpoint mem [x:elt; s:t] : bool := Cases s of
+      nil => false 
+    | (cons y l) => Cases  (E.compare x y) of 
+         (Lt _) => false
+       | (Eq _) => true
+       | (Gt _) => (mem x l)
+       end
+    end.
+
+  Fixpoint add [x:elt; s:t] : t := Cases s of 
+     nil => x::[]
+   | (cons y l) => Cases (E.compare x y) of 
+         (Lt _) => x::s
+       | (Eq _) => s
+       | (Gt _) => y::(add x l)
+     end 
+  end.
+
+  Definition singleton : elt -> t := [x] x::[]. 
+
+  Fixpoint remove [x:elt; s:t] : t := Cases s of 
+     nil => []
+   | (cons y l) => Cases (E.compare x y) of 
+         (Lt _) => s
+       | (Eq _) => l
+       | (Gt _) => y::(remove x l)
+     end 
+  end.  
+  
+  Fixpoint union [s:t] : t -> t := Cases s of 
+    nil => [s']s'
+  | (cons x l) => 
+       Fix union_aux { union_aux / 1 : t -> t := [s']Cases s' of 
+           nil => s
+         | (cons x' l') => Cases (E.compare x x') of 
+              (Lt _ ) => x::(union l s')
+            | (Eq _ ) => x::(union l l')
+            | (Gt _) => x'::(union_aux l')
+            end
+         end}
+   end.      
+
+  Fixpoint inter [s:t] : t -> t := Cases s of 
+    nil => [_] []
+  | (cons x l) => 
+       Fix inter_aux { inter_aux / 1 : t -> t := [s']Cases s' of 
+           nil => []
+         | (cons x' l') => Cases (E.compare x x') of 
+              (Lt _ ) => (inter l s')
+            | (Eq _ ) => x::(inter l l')
+            | (Gt _) => (inter_aux l')
+            end
+         end}
+   end.  
+  
+  Fixpoint diff [s:t] : t -> t := Cases s of 
+    nil => [_] []
+  | (cons x l) => 
+       Fix diff_aux { diff_aux / 1 : t -> t := [s']Cases s' of 
+           nil => s
+         | (cons x' l') => Cases (E.compare x x') of 
+              (Lt _ ) => x::(diff l s')
+            | (Eq _ ) => (diff l l')
+            | (Gt _) => (diff_aux l')
+            end
+         end}
+   end.  
+   
+  Fixpoint equal [s:t] : t -> bool := [s':t]Cases s s' of 
+    nil nil => true
+  | (cons x l) (cons x' l') => Cases (E.compare x x') of 
+       (Eq _) => (equal l l') 
+     | _ => false 
+    end
+  | _ _ => false 
+  end.
+
+  Fixpoint subset [s,s':t] : bool := Cases s s' of 
+    nil _ => true
+  | (cons x l) (cons x' l') => Cases (E.compare x x') of 
+       (Lt _) => false 
+     | (Eq _) => (subset l l') 
+     | (Gt _) => (subset s l')
+    end
+  | _ _ => false 
+  end.
+
+  Fixpoint fold [B:Set; f:elt->B->B; s:t] : B -> B := [i]Cases s of 
+    nil => i
+  | (cons x l) => (f x (fold f l i))
+  end.  
+
+  Fixpoint filter [f:elt->bool; s:t] : t := Cases s of 
+    nil => []
+  | (cons x l) => if (f x) then x::(filter f l) else (filter f l)
+  end.  
+
+  Fixpoint for_all [f:elt->bool; s:t] : bool := Cases s of 
+    nil => true
+  | (cons x l) => if (f x) then (for_all f l) else false
+  end.  
+ 
+  Fixpoint exists [f:elt->bool; s:t] : bool := Cases s of 
+    nil => false
+  | (cons x l) => if (f x) then true else (exists f l)
+  end.
+
+  Fixpoint partition [f:elt->bool; s:t] : t*t := Cases s of 
+     nil => ([],[])
+  | (cons x l) => let (s1,s2) = (partition f l) in 
+                         if (f x) then (x::s1,s2) else (s1,x::s2)
+  end.
+
+  Definition cardinal : t -> nat := [s](fold [_]S s O).
+
+  Definition elements : t -> (list elt) := [x]x.
+
+  Definition min_elt : t -> (option elt) := [s]Cases s of 
+     nil => (None ?)
+   | (cons x _) => (Some ? x)
+  end.
+
+  Fixpoint max_elt  [s:t] : (option elt) := Cases s of 
+    nil => (None ?) 
+   | (cons x nil) => (Some ? x) 
+   | (cons _ l) => (max_elt l)
+  end.
+
+  Definition choose := min_elt.
+
+  (** Proofs of set operation specifications. *)
+
+  Definition In : elt -> t -> Prop := (InList E.eq).
+  Notation "'Sort' l" := (sort E.lt l) (at level 10, l at level 8).
+  Notation "'Inf' x l" := (lelistA E.lt x l) (at level 10, x,l at level 8).
+  Notation "'In' x l" := (InList E.eq x l) (at level 10, x,l at level 8).
+
+  Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
+  Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
+  Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
+  Definition Empty := [s](a:elt)~(In a s).
+  Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
+  Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
+
+  Definition In_eq: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s) := ME.In_eq.
+  Definition Inf_lt : (s:t)(x,y:elt)(E.lt x y) -> (Inf y s) -> (Inf x s) := ME.Inf_lt.
+  Definition Inf_eq : (s:t)(x,y:elt)(E.eq x y) -> (Inf y s) -> (Inf x s) := ME.Inf_eq.
+  Definition In_sort : (s:t)(x,a:elt)(Inf a s) -> (In x s) -> (Sort s) -> (E.lt a x) := ME.In_sort.
+  Hints Resolve Inf_lt Inf_eq. 
+  Hints Immediate In_eq.
+
+  Lemma mem_1: (s:t)(Hs:(Sort s))(x:elt)(In x s) -> (mem x s)=true. 
+  Proof.
+  Induction s; Intros.
+  Inversion H.
+  Inversion_clear Hs.
+  Inversion_clear H0.
+  Simpl; Replace E.compare with X.compare; Auto.
+  Elim (!ME.elim_compare_eq x a); [Intros A B; Rewrite B; Auto | Auto].
+  Simpl; Replace E.compare with X.compare; Auto.
+  Elim (!ME.elim_compare_gt x a); [Intros A B; Rewrite B; Auto | Auto].
+  EApply In_sort; EAuto.
+  Qed.
+
+  Lemma mem_2: (s:t)(x:elt)(mem x s)=true -> (In x s).
+  Proof.
+  Induction s. 
+  Intros; Inversion H.
+  Intros a l Hrec x.
+  Simpl; Elim (E.compare x a); Ground.
+  Inversion H.
+  Qed.
+
+  Lemma add_Inf : (s:t)(x,a:elt)(Inf a s)->(E.lt a x)->(Inf a (add x s)).
+  Proof.
+  Induction s.  
+  Simpl; Intuition.
+  Simpl; Intros; Case (E.compare x a); Intuition; Inversion H0; Intuition.
+  Qed.
+  Hints Resolve add_Inf.
+  
+  Lemma add_sort : (s:t)(Hs:(Sort s))(x:elt)(Sort (add x s)).
+  Proof.
+  Induction  s.
+  Simpl; Intuition.
+  Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear Hs; Auto.
+  Qed. 
+
+  Lemma add_1 : (s:t)(Hs:(Sort s))(x:elt)(In x (add x s)).
+  Proof.
+  Induction s. 
+  Simpl; Intuition.
+  Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear Hs; Ground.
+  Qed.
+
+  Lemma add_2 : (s:t)(Hs:(Sort s))(x,y:elt)(In y s) -> (In y (add x s)).
+  Proof.
+  Induction s. 
+  Simpl; Intuition.
+  Simpl; Intros; Case (E.compare x a); Intuition.
+  Inversion_clear Hs; Inversion_clear H0; EAuto.
+  Qed.
+
+  Lemma add_3 : (s:t)(Hs:(Sort s))(x,y:elt)
+      ~(E.eq x y) -> (In y (add x s)) -> (In y s).
+  Proof.
+  Induction s. 
+  Simpl; Intuition.
+  Inversion_clear H0; Ground; Absurd (E.eq x y); Auto.
+  Simpl; Intros a l Hrec Hs x y; Case (E.compare x a); Intros; 
+   Inversion_clear H0; Inversion_clear Hs; Ground; Absurd (E.eq x y); Auto.
+  Qed.
+
+  Lemma remove_Inf : (s:t)(Hs:(Sort s))(x,a:elt)(Inf a s)->
+  (Inf a (remove x s)).
+  Proof.
+  Induction s.  
+  Simpl; Intuition.
+  Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear H0; Ground.
+  Inversion_clear Hs; Ground; EAuto.
+  Qed.
+  Hints Resolve remove_Inf.
+
+  Lemma remove_sort : (s:t)(Hs:(Sort s))(x:elt)(Sort (remove x s)).
+  Proof.
+  Induction  s.
+  Simpl; Intuition.
+  Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear  Hs; Auto.
+  Qed. 
+
+  Lemma remove_1 : (s:t)(Hs:(Sort s))(x:elt)~(In x (remove x s)).
+  Proof.
+  Induction s. 
+  Simpl; Red; Intros; Inversion H.
+  Simpl; Intros; Case (E.compare x a); Intuition; Inversion_clear Hs. 
+  Inversion_clear H0.
+  Absurd (E.eq x a); Auto. 
+  Absurd (E.lt a x); Auto; EApply In_sort; EAuto.
+  Absurd (E.lt a x); Auto; EApply In_sort; EAuto.
+  Inversion_clear H0; Ground. 
+  Absurd (E.eq x a); Auto.
+  Qed.
+
+  Lemma remove_2 : (s:t)(Hs:(Sort s))(x,y:elt) 
+      ~(E.eq x y) -> (In y s) -> (In y (remove x s)).
+  Proof.
+  Induction s. 
+  Simpl; Intuition.
+  Simpl; Intros; Case (E.compare x a); Intuition; 
+    Inversion_clear Hs; Inversion_clear H1; Auto. 
+  Absurd (E.eq x y); EAuto. 
+  Qed.
+
+  Lemma remove_3 : (s:t)(Hs:(Sort s))(x,y:elt)(In y (remove x s)) -> (In y s).
+  Proof.
+  Induction s. 
+  Simpl; Intuition.
+  Simpl; Intros a l Hrec Hs x y; Case (E.compare x a); Intuition.
+  Inversion_clear Hs; Inversion_clear H; Ground.
+  Qed.
+  
+  Lemma singleton_sort : (x:elt)(Sort (singleton x)).
+  Proof.
+  Unfold singleton; Simpl; Ground.
+  Qed.
+
+  Lemma singleton_1 : (x,y:elt)(In y (singleton x)) -> (E.eq x y).
+  Proof.
+  Unfold singleton; Simpl; Intuition.
+  Inversion_clear H; Auto; Inversion H0.
+  Qed. 
+
+  Lemma singleton_2 : (x,y:elt)(E.eq x y) -> (In y (singleton x)).
+  Proof.
+  Unfold singleton; Simpl; Intuition.
+  Qed. 
+
+  Tactic Definition DoubleInd := 
+    Induction s; 
+    [Simpl; Auto; Try Solve [ Intros; Inversion H ] |
+     Intros x l Hrec; 
+     Induction s'; 
+     [Simpl; Auto; Try Solve [ Intros; Inversion H ] | 
+      Intros x' l' Hrec' Hs Hs'; Inversion Hs; Inversion Hs'; Subst; Simpl]].
+
+  Lemma union_Inf : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(a:elt) 
+      (Inf a s) -> (Inf a s') -> (Inf a (union s s')).
+  Proof.
+  DoubleInd.
+  Intros i His His'; Inversion_clear His; Inversion_clear His'.
+  Case (E.compare x x'); Ground.
+  Qed.
+  Hints Resolve union_Inf.
+ 
+  Lemma union_sort : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Sort (union s s')).
+  Proof.
+  DoubleInd; Case (E.compare x x'); Intuition; Constructor; Auto.
+  EAuto.
+  Change (Inf x' (union x::l l')); Ground.
+  Qed.  
+  
+  Lemma union_1 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) 
+     (In x (union s s')) -> (In x s)\/(In x s').
+  Proof.
+  DoubleInd; Case (E.compare x x'); Intuition; Inversion_clear H; Intuition.
+  Elim (Hrec (x'::l') H1 Hs' x0); Intuition.
+  Elim (Hrec l' H1 H5 x0); Intuition.
+  Elim (H0 x0); Intuition.
+  Qed.
+
+  Lemma union_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) 
+     (In x s) -> (In x (union s s')).
+  Proof.
+  DoubleInd.
+  Intros i Hi; Case (E.compare x x'); Intuition; Inversion_clear Hi; Auto.
+  Qed.
+
+  Lemma union_3 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) 
+     (In x s') -> (In x (union s s')).
+  Proof.
+  DoubleInd. 
+  Intros i Hi; Case (E.compare x x'); Inversion_clear Hi; Intuition; EAuto.
+  Qed.
+    
+  Lemma inter_Inf : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(a:elt) 
+      (Inf a s) -> (Inf a s') -> (Inf a (inter s s')).
+  Proof.
+  DoubleInd.
+  Intros i His His'; Inversion His; Inversion His'; Subst.
+  Case (E.compare x x'); Intuition; EAuto.
+  Qed.
+  Hints Resolve inter_Inf. 
+
+  Lemma inter_sort : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Sort (inter s s')).
+  Proof.
+  DoubleInd; Case (E.compare x x'); EAuto.
+  Qed.  
+  
+  Lemma inter_1 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) 
+     (In x (inter s s')) -> (In x s).
+  Proof.
+  DoubleInd; Case (E.compare x x'); Intuition.
+  EAuto. 
+  Inversion_clear H; EAuto.
+  Qed.
+
+  Lemma inter_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) 
+     (In x (inter s s')) -> (In x s').
+  Proof.
+  DoubleInd; Case (E.compare x x'); Intuition; Inversion_clear H; EAuto. 
+  Qed.
+
+  Lemma inter_3 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) 
+     (In x s) -> (In x s') -> (In x (inter s s')).
+  Proof.
+  DoubleInd.
+  Intros i His His'; Elim (E.compare x x'); Intuition.
+
+  Inversion_clear His. 
+  Absurd (E.lt i x); EAuto.
+  Apply In_sort with (x'::l'); Auto.
+  Constructor; EApply ME.eq_lt; EAuto.
+  EApply In_eq; EAuto.
+  EApply In_eq; EAuto.
+
+  Inversion_clear His; [ EAuto | Inversion_clear His' ]; EAuto.
+
+  Change (In i (inter x::l l')). 
+  Inversion_clear His'.
+  Absurd (E.lt i x'); EAuto.
+  Apply In_sort with (x::l); Auto. 
+  Constructor; EApply ME.eq_lt; EAuto.
+  EApply In_eq; EAuto.
+  EApply In_eq; EAuto.
+  Qed.
+
+  Lemma diff_Inf : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(a:elt) 
+      (Inf a s) -> (Inf a s') -> (Inf a (diff s s')).
+  Proof.
+  DoubleInd.
+  Intros i His His'; Inversion His; Inversion His'.
+  Case (E.compare x x'); Intuition;EAuto.
+  Qed.
+  Hints Resolve diff_Inf. 
+
+  Lemma diff_sort : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Sort (diff s s')).
+  Proof.
+  DoubleInd; Case (E.compare x x'); EAuto.
+  Qed.  
+  
+  Lemma diff_1 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) 
+     (In x (diff s s')) -> (In x s).
+  Proof.
+  DoubleInd; Case (E.compare x x'); Intuition.
+  Inversion_clear H;  EAuto.
+  EAuto.
+  Qed.
+
+  Lemma diff_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) 
+     (In x (diff s s')) -> ~(In x s').
+  Proof.
+  DoubleInd.
+  Intros; Intro Abs; Inversion Abs. 
+  Case (E.compare x x'); Intuition.
+
+  Inversion_clear H.
+  Absurd (E.lt x x); EAuto. 
+  Apply In_sort with (x'::l'); Auto. 
+  EApply In_eq; EAuto.
+  EAuto.
+  
+  Inversion_clear H3.
+  Generalize (diff_1 H1 H5 H); Intros. 
+  Absurd (E.lt x x0); EAuto.
+  Apply In_sort with l; EAuto.
+  EAuto.
+  
+  Inversion_clear H3. 
+  Generalize (diff_1 Hs H5 H); Intros. 
+  Absurd (E.lt x' x'); EAuto.
+  Apply In_sort with (x::l); Auto.
+  EApply In_eq; EAuto.
+  EAuto.  
+  Qed.
+
+  Lemma diff_3 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt) 
+     (In x s) -> ~(In x s') -> (In x (diff s s')).
+  Proof.
+  DoubleInd.
+  Intros i His His'; Elim (E.compare x x'); Intuition; Inversion_clear His.
+  EAuto.
+  EAuto.
+  Elim His'; EAuto.
+  EAuto.
+  Qed.  
+
+  Lemma equal_1: (s,s':t)(Hs:(Sort s))(Hs':(Sort s')) 
+     (Equal s s') -> (equal s s')=true.
+  Proof.
+  Induction s; Unfold Equal.
+  Intro s'; Case s'; Auto.
+  Simpl; Intuition.
+  Elim (H e); Intros; Assert A : (In e []); Auto; Inversion A.
+  Intros x l Hrec s'.
+  Case s'.
+  Intros; Elim (H x); Intros; Assert A : (In x []); Auto; Inversion A.
+  Intros x' l' Hs Hs'; Inversion Hs; Inversion Hs'; Subst.
+  Simpl; Case (E.compare x); Intros; Auto.
+
+  Elim (H  x); Intros.
+  Assert A : (In x x'::l'); Auto; Inversion_clear A.
+  Absurd (E.eq x x'); EAuto.
+  Absurd (E.lt x' x); Auto.
+  Apply In_sort with l';EAuto.
+  
+  Apply Hrec; Intuition; Elim (H a); Intros.
+  Assert A : (In a x'::l'); Auto; Inversion_clear A; Auto.
+  Absurd (E.lt x' x); Auto. 
+  Apply In_sort with l;Auto; 
+    [ Apply Inf_eq with x;Auto | Apply In_eq with a; EAuto ].
+  Assert A : (In a x::l); Auto; Inversion_clear A; Auto.
+  Absurd (E.lt x x'); Auto. 
+  Apply In_sort with l';Auto; 
+    [ Apply Inf_eq with x';Auto | Apply In_eq with a; EAuto ].
+
+  Elim (H  x'); Intros.
+  Assert A : (In x' x::l); Auto; Inversion_clear A.
+  Absurd (E.eq x' x); EAuto.
+  Absurd (E.lt x x'); Auto.
+  Apply In_sort with l;EAuto.
+  Qed.
+
+  Lemma equal_2: (s,s':t)(equal s s')=true -> (Equal s s').
+  Proof.
+  Induction s; Unfold Equal.
+  Intro s'; Case s'; Intros.
+  Intuition.
+  Simpl in H; Discriminate H.
+  Intros x l Hrec s'.
+  Case s'.
+  Intros; Simpl in H; Discriminate H.
+  Intros x' l'; Simpl; Case (E.compare x); Intros; Auto.
+  Discriminate H.
+  Elim (Hrec l' H a); Intuition; Inversion_clear H2; EAuto.
+  Discriminate H.  
+  Qed.  
+  
+  Lemma subset_1: (s,s':t)(Hs:(Sort s))(Hs':(Sort s')) 
+     (Subset s s') -> (subset s s')=true.
+  Proof.
+  Intros s s'; Generalize s' s; Clear s s'.
+  Induction s'; Unfold Subset.
+  Intro s; Case s; Auto.
+  Intros; Elim (H e); Intros; Assert A : (In e []); Auto; Inversion A. 
+  Intros x' l' Hrec s; Case s.
+  Simpl; Auto.
+  Intros x l Hs Hs'; Inversion Hs; Inversion Hs'; Subst.
+  Simpl; Case (E.compare x); Intros; Auto.
+
+  Assert A : (In x x'::l'); Auto; Inversion_clear A.
+  Absurd (E.eq x x'); EAuto.
+  Absurd (E.lt x' x); Auto.
+  Apply In_sort with l';EAuto.
+  
+  Apply Hrec; Intuition.
+  Assert A : (In a x'::l'); Auto; Inversion_clear A; Auto.
+  Absurd (E.lt x' x); Auto. 
+  Apply In_sort with l;Auto; [ Apply Inf_eq with x;Auto | Apply In_eq with a; EAuto ].
+
+  Apply Hrec; Intuition.
+  Assert A : (In a x'::l'); Auto; Inversion_clear A; Auto.
+  Inversion_clear H0.  
+  Absurd (E.lt x' x); EAuto.
+  Absurd (E.lt x x'); Auto. 
+  Apply In_sort with l;EAuto.
+  Qed.
+
+  Lemma subset_2: (s,s':t)(subset s s')=true -> (Subset s s').
+  Proof.
+  Intros s s'; Generalize s' s; Clear s s'.
+  Induction s'; Unfold Subset.
+  Intro s; Case s; Auto.
+  Simpl; Intros; Discriminate H.
+  Intros x' l' Hrec s; Case s.
+  Intros; Inversion H0.
+  Intros x l; Simpl; Case (E.compare x); Intros; Auto.
+  Discriminate H.  
+  Inversion_clear H0; EAuto.
+  EAuto.
+  Qed.  
+  
+  Lemma empty_sort : (Sort empty).
+  Proof.
+  Unfold empty; Constructor.
+  Qed.
+
+  Lemma empty_1 : (Empty empty).
+  Proof.
+  Unfold Empty empty; Intuition; Inversion H.
+  Qed. 
+
+  Lemma is_empty_1 : (s:t)(Empty s) -> (is_empty s)=true.
+  Proof.
+  Unfold Empty; Intro s; Case s; Simpl; Intuition.
+  Elim (H e); Auto.
+  Qed.
+  
+  Lemma is_empty_2 : (s:t)(is_empty s)=true -> (Empty s). 
+  Proof.
+  Unfold Empty; Intro s; Case s; Simpl; Intuition; Inversion H0.
+  Qed.
+
+  Lemma elements_1: (s:t)(x:elt)(In x s) -> (InList E.eq x (elements s)).
+  Proof.
+  Unfold elements; Auto.
+  Qed.
+
+  Lemma elements_2: (s:t)(x:elt)(InList E.eq x (elements s)) -> (In x s).
+  Proof. 
+  Unfold elements; Auto.
+  Qed.
+ 
+  Lemma elements_3: (s:t)(Hs:(Sort s))(sort E.lt (elements s)).  
+  Proof. 
+  Unfold elements; Auto.
+  Qed.
+
+  Lemma min_elt_1: (s:t)(x:elt)(min_elt s) = (Some ? x) -> (In x s). 
+  Proof.
+  Intro s; Case s; Simpl; Intros; Inversion H; Auto.
+  Qed.  
+
+  Lemma min_elt_2: (s:t)(Hs:(Sort s))(x,y:elt)
+      (min_elt s) = (Some ? x) -> (In y s) -> ~(E.lt y x). 
+  Proof.
+  Induction s; Simpl.
+  Intros; Inversion H.
+  Intros a l; Case l; Intros; Inversion H0; Inversion_clear H1; Subst. 
+  EAuto.
+  Inversion H2.
+  EAuto.
+  Inversion_clear Hs.
+  Inversion_clear H3.
+  Intro; Absurd (E.lt y e); EAuto.
+  Qed. 
+
+  Lemma min_elt_3: (s:t)(min_elt s) = (None ?) -> (Empty s).
+  Proof.
+  Unfold Empty; Intro s; Case s; Simpl; Intuition; Inversion H; Inversion H0.
+  Qed.
+
+  Lemma max_elt_1: (s:t)(x:elt)(max_elt s) = (Some ? x) -> (In x s). 
+  Proof. 
+  Induction s; Simpl.
+  Intros; Inversion H.
+  Intros x l; Case l; Simpl.
+  Intuition.
+  Inversion H0; Auto.
+  EAuto.
+  Qed.
+ 
+  Lemma max_elt_2: (s:t)(Hs:(Sort s))(x,y:elt)
+     (max_elt s) = (Some ? x) -> (In y s) -> ~(E.lt x y). 
+  Proof.
+  Induction s; Simpl.
+  Intros; Inversion H.
+  Intros x l; Case l; Simpl.
+  Intuition.
+  Inversion H0; Subst.
+  Inversion_clear H1.
+  Absurd (E.eq y x0); Auto. 
+  Inversion H3.
+  Intros; Inversion_clear Hs; Inversion_clear H3; Inversion_clear H1.
+  Assert ~(E.lt x0 e).
+   EApply H; EAuto.
+  Intro.
+  Elim H1; Apply E.lt_trans with x; Auto; EApply ME.lt_eq; EAuto.
+  EApply H;EAuto.
+  Qed. 
+
+  Lemma max_elt_3: (s:t)(max_elt s) = (None ?) -> (Empty s).
+  Proof.
+  Unfold Empty; Induction s; Simpl.
+  Red; Intros; Inversion H0.
+  Intros x l; Case l; Simpl; Intros.
+  Inversion H0.
+  Elim (H H0 e); Auto.
+  Qed.
+
+  Definition choose_1:
+     (s:t)(x:elt)(choose s)=(Some ? x) -> (In x s)
+     := min_elt_1.
+
+  Definition choose_2: (s:t)(choose s)=(None ?) -> (Empty s)
+     := min_elt_3.
+
+  Lemma fold_1 : (s:t)(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; Intro s; Case s; Intros; Simpl; Intuition; Elim (H e); Auto.
+  Qed.
+
+  Lemma fold_equal : 
+     (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(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) -> (Equal s s') ->
+     (eqA (fold f s i) (fold f s' i)).
+  Proof.
+  Induction s; Unfold Equal; Simpl.
+
+  Intro s'; Case s'; Intuition.
+  Intros.
+  Elim (H1 e); Intuition.
+  Assert X : (In e []); Auto; Inversion X.
+
+  Intros x l Hrec s'; Case s'.
+  Intros.
+  Elim (H1 x); Intuition.
+  Assert X : (In x []); Auto; Inversion X.
+  Simpl; Intros x' l' Hs Hs' a; Intros.
+  Inversion_clear Hs; Inversion_clear Hs'.
+  Assert (E.eq x x').
+   Assert (In x x'::l').
+    Elim (H1 x); Auto.
+   Assert (In x' x::l).
+    Elim (H1 x'); Auto.
+  Inversion_clear H6; Auto.
+  Inversion_clear H7; Auto.
+  Absurd (E.lt x x').
+  Apply ME.lt_not_gt.
+  Apply In_sort with l'; EAuto.
+  Apply In_sort with l; EAuto.
+  Apply H; Auto.
+  Apply (Hrec l' H2 H4 a eqA); Auto.
+  (* To prove (Equal l l') *)
+  Intuition.
+  Elim (H1 a0); Intros.
+  Assert (In a0 x'::l'). Auto.
+  Inversion_clear H10; Auto.
+  Intros; Absurd (E.lt x x'); EAuto.
+  Apply In_sort with l; EAuto.
+  Elim (H1 a0); Intros.
+  Assert (In a0 x::l). Auto.
+  Inversion_clear H10; Auto.
+  Intros; Absurd (E.lt x' x); EAuto.
+  Apply In_sort with l'; EAuto.
+  Qed.
+
+  Lemma fold_2 : 
+     (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)(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.
+  Induction s; Unfold Add; Simpl.
+
+  Intro s'; Case s'.
+  Intros.
+  Elim (H2 x); Intuition.
+  Assert X : (In x []); Auto; Inversion X.
+  Simpl; Intros.
+  Inversion_clear Hs'.
+  Apply H; Auto.
+  Elim (H2 e);Intuition.
+  Elim H5; Auto.
+  Intros X; Inversion X.
+  Apply fold_1; Auto.
+  Unfold Empty; Intuition.
+  Assert (y:elt)(In y e::l) -> (E.eq y x).
+   Intros; Elim (H2 y); Intuition; Inversion H7.
+  Assert (E.eq a x); [Ground | Idtac].
+  Assert (E.eq e x); [Ground | Idtac].
+  Absurd (E.lt a e); EAuto.
+  Apply In_sort with l; EAuto. Apply In_eq with a; EAuto.
+
+  Intros x l Hrec s'; Case s'.
+  Intros.
+  Elim (H2 x0); Intuition.
+  Assert X : (In x0 []); Auto; Inversion X.
+  Simpl; Intros x' l' Hs Hs' a; Intros.
+  Inversion Hs; Inversion Hs'.
+  Assert (In a x'::l');[Ground|Idtac].
+  (* 2 cases: x'=a or x'<a *)
+  (* first, x'=a *)
+  Inversion_clear H11.
+  Apply H; Auto.
+  Change (eqA (fold f l' i) (fold f (x::l) i)).
+  Apply (!fold_equal l' (x::l) H9 Hs A eqA); Auto.
+  (* To prove that (Equal l' (x::l)) *)
+  Unfold Equal.
+  Intuition.
+  Elim (H2 a2); Intros.
+  Elim H13; Auto.
+  Intros.
+  Absurd (E.lt x' a2); EAuto; Apply In_sort with l'; EAuto.
+   Elim (H2 a2); Intros.
+  Assert (In a2 x'::l'); Auto.
+  Inversion_clear H15; Auto.
+  Elim H1; Apply In_eq with a2; EAuto.
+ (* second, x'<a *)
+  Assert (E.lt x' a).
+    Apply In_sort with l'; EAuto.
+  Assert ~(E.eq a x).
+   Intro; Elim H1; Auto.
+  Assert (E.eq x x').
+   Assert (In x x'::l').
+    Elim (H2 x); Auto.
+   Assert (In x' x::l).
+    Elim (H2 x'); Intuition.
+    Elim H15; Auto.
+    Intros; Absurd (E.eq x' a); EAuto.
+   Inversion_clear H14; Auto.
+   Inversion_clear H15; Auto.
+   Absurd (E.lt x x').
+   Apply ME.lt_not_gt.
+   Apply In_sort with l'; EAuto.
+   Apply In_sort with l; EAuto.
+  Apply (Seq_trans ? ? st) with (f x (f a (fold f l i))).
+  2: Apply H0.
+  Apply H; Auto.
+  Apply (Hrec l' H5 H9 a A eqA); Clear Hrec; Auto.
+  (* To prove (Add a l l') *)
+  Intuition.
+  Elim (H2 y); Intros.
+  Elim H16; Auto; Intros.
+  Inversion_clear H18.
+  Absurd (E.lt x' y); EAuto; Apply In_sort with l'; EAuto.
+  Right; Auto.
+  Apply In_eq with a; Auto.
+  Elim (H2 y); Intuition.
+  Assert (In y x'::l'); Auto.
+  Inversion_clear H17; Auto.
+  Absurd (E.lt x y); EAuto; Apply In_sort with l; EAuto.
+  Qed.
+
+  Lemma cardinal_1 : (s:t)(Empty s) -> (cardinal s)=O.
+  Proof.
+  Unfold cardinal; Intros; Apply fold_1; Auto.
+  Intuition EAuto; Transitivity y; Auto.
+  Qed.
+
+  Lemma cardinal_2 : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(x:elt)
+     ~(In x s) -> (Add  x s s') -> (cardinal s') = (S (cardinal s)).
+  Proof.
+  Unfold cardinal; Intros.
+  Assert (compat_op E.eq (eq ?) [_]S).
+   Unfold compat_op; Auto.
+  Assert (transpose (eq ?) [_:elt]S).
+    Unfold transpose; Auto.
+  Refine (!fold_2 s s' Hs Hs' x nat (eq ?) ? O [_]S H1 H2 H H0).
+  Intuition EAuto; Transitivity y; Auto.
+  Qed.
+
+  Lemma filter_Inf : 
+    (s:t)(Hs:(Sort s))(x:elt)(f:elt->bool)(Inf x s) -> (Inf x (filter f s)).
+  Proof.
+  Induction s; Simpl.
+  Intuition.  
+  Intros x l Hrec Hs a f Ha; Inversion_clear Hs; Inversion Ha.
+  Case (f x); [Constructor; Auto | EAuto]. 
+  Qed.
+
+  Lemma filter_sort : (s:t)(Hs:(Sort s))(f:elt->bool)(Sort (filter f s)).
+  Proof.
+  Induction s; Simpl.
+  Auto.
+  Intros x l Hrec Hs f; Inversion_clear Hs.
+  Case (f x); Auto.
+  Constructor; Auto.
+  Apply filter_Inf; Auto. 
+  Qed.
+
+  Lemma filter_1: (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) -> 
+     (In x (filter f s)) -> (In x s).
+  Proof.
+  Induction s; Simpl.
+  Intros; Inversion H0.
+  Intros x l Hrec a f Hf.
+  Case (f x); Simpl; Ground.
+  Inversion H; Ground.
+  Qed.
+
+   Lemma filter_2: 
+    (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) ->(In x (filter f s)) -> 
+    (f x)=true.   
+   Proof.
+  Induction s; Simpl.
+  Intros; Inversion H0.
+  Intros x l Hrec a f Hf.
+  Generalize (Hf x); Case (f x); Simpl; Ground.
+  Inversion H0; Ground.
+  Symmetry; Ground.
+  Qed.
+ 
+  Lemma filter_3: 
+    (s:t)(x:elt)(f:elt->bool)(compat_bool E.eq f) -> 
+        (In x s) -> (f x)=true -> (In x (filter f s)).     
+  Proof.
+  Induction s; Simpl.
+  Intros; Inversion H0.
+  Intros x l Hrec a f Hf.
+  Generalize (Hf x); Case (f x); Simpl; Ground; Inversion H0; Ground.
+  Rewrite <- (H a) in H1; Auto; Discriminate H1.
+  Qed.
+
+  Lemma for_all_1: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> 
+       (For_all [x](f x)=true s) -> (for_all f s)=true.
+  Proof. 
+  Induction s; Simpl; Auto; Unfold For_all.
+  Intros x l Hrec f Hf. 
+  Generalize (Hf x); Case (f x); Simpl; Ground. 
+  Rewrite (H x); Auto.
+  Qed.
+
+  Lemma for_all_2: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> (for_all f s)=true -> 
+    (For_all [x](f x)=true s).
+  Proof. 
+  Induction s; Simpl; Auto; Unfold For_all.
+  Intros; Inversion H1.
+  Intros x l Hrec f Hf. 
+  Intros A a; Intros. 
+  Assert (f x)=true.
+   Generalize A; Case (f x); Auto.
+  Rewrite H0 in A; Simpl in A.
+  Inversion H; Ground.
+  Rewrite (Hf a x); Auto.
+  Qed.
+
+  Lemma exists_1: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> (Exists [x](f x)=true s) -> 
+    (exists f s)=true.
+  Proof.
+  Induction s; Simpl; Auto; Unfold Exists.
+  Intros.
+  Elim H0; Intuition. 
+  Inversion H2.
+  Intros x l Hrec f Hf. 
+  Generalize (Hf x); Case (f x); Simpl; Ground. 
+  Inversion_clear H0.
+  Absurd (false=true); Auto with bool.
+  Rewrite (H x); Auto.
+  Rewrite <- H1.
+  Ground.
+  Ground.
+  Qed.
+
+  Lemma exists_2: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> (exists f s)=true -> 
+    (Exists [x](f x)=true s).
+  Proof. 
+  Induction s; Simpl; Auto; Unfold Exists.
+  Intros; Discriminate.
+  Intros x l Hrec f Hf.
+  Generalize (refl_equal ? (f x)); Pattern -1 (f x); Case (f x). 
+  Intros; Exists x; Auto.
+  Intros; Elim (Hrec f); Auto; Ground.
+  Qed.
+
+  Lemma partition_Inf_1 : 
+     (s:t)(Hs:(Sort s))(f:elt->bool)(x:elt)(Inf x s) -> 
+     (Inf x (fst ? ? (partition f s))).
+  Proof.
+  Induction s; Simpl.
+  Intuition.  
+  Intros x l Hrec Hs f a Ha; Inversion_clear Hs; Inversion Ha.
+  Generalize (Hrec H f a).
+  Case (f x); Case (partition f l); Simpl.
+  Intros; Constructor; Auto.
+  EAuto.
+  Qed.
+
+  Lemma partition_Inf_2 : 
+     (s:t)(Hs:(Sort s))(f:elt->bool)(x:elt)(Inf x s) -> 
+     (Inf x (snd ? ? (partition f s))).
+  Proof.
+  Induction s; Simpl.
+  Intuition.  
+  Intros x l Hrec Hs f a Ha; Inversion_clear Hs; Inversion Ha.
+  Generalize (Hrec H f a).
+  Case (f x); Case (partition f l); Simpl.
+  EAuto.
+  Intros; Constructor; Auto.
+  Qed.
+
+  Lemma partition_sort_1 : (s:t)(Hs:(Sort s))(f:elt->bool)
+    (Sort (fst ? ? (partition f s))).
+  Proof.
+  Induction s; Simpl.
+  Auto.
+  Intros x l Hrec Hs f; Inversion_clear Hs.
+  Generalize (Hrec H f); Generalize (partition_Inf_1 H f).
+  Case (f x); Case (partition f l); Simpl; Auto.
+  Qed.
+  
+  Lemma partition_sort_2 : (s:t)(Hs:(Sort s))(f:elt->bool)
+     (Sort (snd ? ? (partition f s))).
+  Proof.
+  Induction s; Simpl.
+  Auto.
+  Intros x l Hrec Hs f; Inversion_clear Hs.
+  Generalize (Hrec H f); Generalize (partition_Inf_2 H f).
+  Case (f x); Case (partition f l); Simpl; Auto.
+  Qed.
+
+  Lemma partition_1: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> 
+    (Equal (fst ? ? (partition f s)) (filter f s)).
+  Proof.
+  Induction s; Simpl; Auto; Unfold Equal.
+  Ground.
+  Intros x l Hrec f Hf.
+  Generalize (Hrec f Hf); Clear Hrec.
+  Case (partition f l); Intros s1 s2; Simpl; Intros.
+  Case (f x); Simpl; Ground; Inversion H0;  Intros; Ground. 
+  Qed.
+   
+  Lemma partition_2: 
+    (s:t)(f:elt->bool)(compat_bool E.eq f) -> 
+    (Equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s)).
+  Proof.
+  Induction s; Simpl; Auto; Unfold Equal.
+  Ground.
+  Intros x l Hrec f Hf. 
+  Generalize (Hrec f Hf); Clear Hrec.
+  Case (partition f l); Intros s1 s2; Simpl; Intros.
+  Case (f x); Simpl; Ground; Inversion H0; Intros; Ground. 
+  Qed.
+ 
+  Definition eq : t -> t -> Prop := Equal.
+
+  Lemma eq_refl: (s:t)(eq s s). 
+  Proof. 
+  Unfold eq Equal; Intuition.
+  Qed.
+
+  Lemma eq_sym: (s,s':t)(eq s s') -> (eq s' s).
+  Proof. 
+  Unfold eq Equal; Ground.
+  Qed.
+
+  Lemma eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s'').
+  Proof. 
+  Unfold eq Equal; Ground.
+  Qed.
+
+  Inductive lt : t -> t -> Prop := 
+     lt_nil : (x:elt)(s:t)(lt [] (x::s)) 
+   | lt_cons_lt : (x,y:elt)(s,s':t)(E.lt x y) -> (lt (x::s) (y::s'))
+   | lt_cons_eq :  (x,y:elt)(s,s':t)(E.eq x y) -> (lt s s') -> (lt (x::s) (y::s')).
+  Hint lt := Constructors lt.
+   
+  Lemma lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s'').
+  Proof. 
+  Intros s s' s'' H; Generalize s''; Clear s''; Elim H.
+  Intros x l s'' H'; Inversion_clear H'; Auto.
+  Intros x x' l l' E s'' H'; Inversion_clear H'; Auto. 
+  EAuto.
+  Constructor 2; Apply ME.lt_eq with x'; Auto.
+  Intros.
+  Inversion_clear H3.
+  Constructor 2; Apply ME.eq_lt with y; Auto.
+  Constructor 3; EAuto.  
+  Qed. 
+
+  Lemma lt_not_eq : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(lt s s') -> ~(eq s s').
+  Proof. 
+  Unfold eq Equal. 
+  Intros s s' Hs Hs' H; Generalize Hs Hs'; Clear Hs Hs'; Elim H; Intros; Intro.
+  Elim (H0 x); Intros.
+  Assert X : (In x []); Auto; Inversion X.
+  Inversion_clear Hs; Inversion_clear Hs'.
+  Elim (H1 x); Intros. 
+  Assert X : (In x y::s'0); Auto; Inversion_clear X.
+  Absurd (E.eq x y); EAuto.
+  Absurd (E.lt y x); Auto.
+  EApply In_sort; EAuto.
+  Inversion_clear Hs; Inversion_clear Hs'.
+  Elim H2; Auto; Intuition.
+  Elim (H3 a); Intros.
+  Assert X: (In a y::s'0); Auto; Inversion_clear X; Auto.
+  Absurd (E.lt x a); EAuto.
+  EApply In_sort with s0; EAuto.
+  Elim (H3 a); Intros.
+  Assert X: (In a x::s0); Auto; Inversion_clear X; Auto.
+  Absurd (E.lt y a); EAuto.
+  EApply In_sort with s'0; EAuto.
+  Qed.
+
+  Definition compare : (s,s':t)(Hs:(Sort s))(Hs':(Sort s'))(Compare lt eq s s').
+  Proof.
+  Induction s.
+  Intros; Case s'. 
+  Constructor 2; Apply eq_refl. 
+  Constructor 1; Auto.
+  Intros a l Hrec s'; Case s'.
+  Constructor 3; Auto.
+  Intros a' l' Hs Hs'.
+  Case (E.compare a a'); [ Constructor 1 | Idtac | Constructor 3 ]; Auto.
+  Elim (Hrec l'); [ Constructor 1 | Constructor 2 | Constructor 3 | Inversion Hs | Inversion Hs']; Auto.
+  Generalize e; Unfold eq Equal; Intuition; 
+    Inversion_clear H; EAuto; Elim (e1 a0); Auto.
+  Defined.
+
+End Raw.
+
+(** Now, in order to really provide a functor implementing S, we 
+   need to encapsulate everything into a type of strictly ordered lists. *)
+
+Module Make [X:OrderedType] <: S with Module E := X.
+
+ Module E := X.
+ Module Raw := (Raw X). 
+
+ Record slist : Set := { this :> Raw.t ; sorted : (sort E.lt this) }.
+ Definition t := slist. 
+ Definition elt := X.t.
+ 
+ Definition In := [x:elt;s:t](Raw.In x s).
+ Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
+ Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
+ Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
+ Definition Empty := [s](a:elt)~(In a s).
+ Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
+ Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
+  
+ Definition In_1 := [s:t](!Raw.In_eq s).
+ 
+ Definition mem := [x:elt;s:t](Raw.mem x s).
+ Definition mem_1 := [s:t](Raw.mem_1 (sorted s)). 
+ Definition mem_2 := [s:t](!Raw.mem_2 s).
+
+ Definition add := [x,s](Build_slist (Raw.add_sort (sorted s) x)).
+ Definition add_1 :=  [s:t](Raw.add_1 (sorted s)).
+ Definition add_2 := [s:t](Raw.add_2 (sorted s)).
+ Definition add_3 := [s:t](Raw.add_3 (sorted s)).
+
+ Definition remove := [x,s](Build_slist (Raw.remove_sort (sorted s) x)).
+ Definition remove_1 :=  [s:t](Raw.remove_1 (sorted s)).
+ Definition remove_2 := [s:t](Raw.remove_2 (sorted s)).
+ Definition remove_3 := [s:t](Raw.remove_3 (sorted s)).
+ 
+ Definition singleton := [x](Build_slist (Raw.singleton_sort x)).
+ Definition singleton_1 := Raw.singleton_1.
+ Definition singleton_2 := Raw.singleton_2.
+  
+ Definition union := [s,s':t](Build_slist (Raw.union_sort (sorted s) (sorted s'))). 
+ Definition union_1 := [s,s':t](Raw.union_1 (sorted s) (sorted s')).
+ Definition union_2 := [s,s':t](Raw.union_2 (sorted s) (sorted s')).
+ Definition union_3 := [s,s':t](Raw.union_3 (sorted s) (sorted s')).
+
+ Definition inter :=[s,s':t](Build_slist (Raw.inter_sort (sorted s) (sorted s'))). 
+ Definition inter_1 := [s,s':t](Raw.inter_1 (sorted s) (sorted s')).
+ Definition inter_2 := [s,s':t](Raw.inter_2 (sorted s) (sorted s')).
+ Definition inter_3 := [s,s':t](Raw.inter_3 (sorted s) (sorted s')).
+ 
+ Definition diff :=[s,s':t](Build_slist (Raw.diff_sort (sorted s) (sorted s'))). 
+ Definition diff_1 := [s,s':t](Raw.diff_1 (sorted s) (sorted s')).
+ Definition diff_2 := [s,s':t](Raw.diff_2 (sorted s) (sorted s')).
+ Definition diff_3 := [s,s':t](Raw.diff_3 (sorted s) (sorted s')).
+ 
+ Definition equal := [s,s':t](Raw.equal s s'). 
+ Definition equal_1 := [s,s':t](Raw.equal_1 (sorted s) (sorted s')).  
+ Definition equal_2 := [s,s':t](!Raw.equal_2 s s').
+ 
+ Definition subset := [s,s':t](Raw.subset s s').
+ Definition subset_1 := [s,s':t](Raw.subset_1 (sorted s) (sorted s')).  
+ Definition subset_2 := [s,s':t](!Raw.subset_2 s s').
+
+ Definition empty := (Build_slist Raw.empty_sort).
+ Definition empty_1 := Raw.empty_1.
+ 
+ Definition is_empty := [s:t](Raw.is_empty s).
+ Definition is_empty_1 := [s:t](!Raw.is_empty_1 s).
+ Definition is_empty_2 := [s:t](!Raw.is_empty_2 s).
+
+ Definition elements := [s:t](Raw.elements s).
+ Definition elements_1 := [s:t](!Raw.elements_1 s).
+ Definition elements_2 := [s:t](!Raw.elements_2 s).
+ Definition elements_3 := [s:t](Raw.elements_3 (sorted s)).
+ 
+ Definition min_elt := [s:t](Raw.min_elt s).
+ Definition min_elt_1 := [s:t](!Raw.min_elt_1 s).
+ Definition min_elt_2 := [s:t](Raw.min_elt_2 (sorted s)).
+ Definition min_elt_3 := [s:t](!Raw.min_elt_3 s).
+
+ Definition max_elt := [s:t](Raw.max_elt s).
+ Definition max_elt_1 := [s:t](!Raw.max_elt_1 s).
+ Definition max_elt_2 := [s:t](Raw.max_elt_2 (sorted s)).
+ Definition max_elt_3 := [s:t](!Raw.max_elt_3 s).
+  
+ Definition choose := min_elt.
+ Definition choose_1 := min_elt_1.
+ Definition choose_2 := min_elt_3.
+ 
+ Definition fold := [B:Set; f: elt->B->B; s:t](!Raw.fold B f s). 
+ Definition fold_1 := [s:t](!Raw.fold_1 s). 
+ Definition fold_2 := [s,s':t](Raw.fold_2 (sorted s) (sorted s')).
+ 
+ Definition cardinal := [s:t](Raw.cardinal s).
+ Definition cardinal_1 := [s:t](!Raw.cardinal_1 s). 
+ Definition cardinal_2 := [s,s':t](Raw.cardinal_2 (sorted s) (sorted s')).
+ 
+ Definition filter := [f: elt->bool; s:t](Build_slist (Raw.filter_sort (sorted s) f)).
+ Definition filter_1 := [s:t](!Raw.filter_1 s).
+ Definition filter_2 := [s:t](!Raw.filter_2 s).
+ Definition filter_3 := [s:t](!Raw.filter_3 s).
+ 
+ Definition for_all := [f:elt->bool; s:t](Raw.for_all f s).
+ Definition for_all_1 := [s:t](!Raw.for_all_1 s). 
+ Definition for_all_2 := [s:t](!Raw.for_all_2 s). 
+
+ Definition exists := [f:elt->bool; s:t](Raw.exists f s).
+ Definition exists_1 := [s:t](!Raw.exists_1 s). 
+ Definition exists_2 := [s:t](!Raw.exists_2 s). 
+
+ Definition partition := [f:elt->bool; s:t]
+    let p = (Raw.partition f s) in  
+    ((!Build_slist (fst ?? p) (Raw.partition_sort_1 (sorted s) f)), 
+     (!Build_slist (snd ?? p) (Raw.partition_sort_2 (sorted s) f))).
+ Definition partition_1 := [s:t](!Raw.partition_1 s).
+ Definition partition_2 := [s:t](!Raw.partition_2 s). 
+
+ Definition eq := [s,s':t](Raw.eq s s').
+ Definition eq_refl := [s:t](Raw.eq_refl s).
+ Definition eq_sym := [s,s':t](!Raw.eq_sym s s').
+ Definition eq_trans := [s,s',s'':t](!Raw.eq_trans s s' s'').
+  
+ Definition lt := [s,s':t](Raw.lt s s').
+ Definition lt_trans := [s,s',s'':t](!Raw.lt_trans s s' s'').
+ Definition lt_not_eq := [s,s':t](Raw.lt_not_eq (sorted s) (sorted s')).
+
+ Definition compare : (s,s':t)(Compare lt eq s s').
+ Proof.
+ Intros; Elim (Raw.compare (sorted s) (sorted s')); 
+  [Constructor 1 | Constructor 2 | Constructor 3]; Auto. 
+ Defined.
+
+End Make.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
new file mode 100644
index 0000000000..226205877c
--- /dev/null
+++ b/theories/FSets/FSetProperties.v
@@ -0,0 +1,1483 @@
+(***********************************************************************)
+(*  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$ *)
+
+(** This module proves many properties of finite sets that 
+    are consequences of the axiomatization in [FSetInterface] *) 
+
+Require Omega.
+
+Import nat_scope.
+Open Scope nat_scope.
+
+Require Export FSetInterface. 
+Require Export Bool.
+Require Export Sumbool.
+Require Export Zerob. 
+Set Implicit Arguments.
+
+(* For proving (Setoid_Theory ? (eq ?)) *)
+Tactic Definition ST :=
+  Constructor; Intros;[ Trivial | Symmetry; Trivial | EApply trans_eq; EAuto ].
+Hint st : core := Extern 1 (Setoid_Theory ? (eq ?)) ST.
+
+Definition gen_st : (A:Set)(Setoid_Theory ? (eq A)).
+Auto.
+Qed.
+
+
+Module Properties [M:S].
+  Import M.
+  Import Logic. (* for unmasking eq. *)  
+  Import Peano. (* for unmasking lt *)
+  
+  Module ME := MoreOrderedType E.  
+
+  Section Old_Spec_Now_Properties. 
+
+  Variable s,s' : t.
+  Variable x,y,z : elt.
+
+  Lemma mem_eq: 
+    (E.eq x y) -> (mem x s)=(mem y s).
+  Proof. 
+  Intros; Apply bool_1.
+  Generalize (!mem_1 s x) (!mem_1 s y) (!mem_2 s x) (!mem_2 s y).
+  Intuition. 
+  EAuto.
+  Apply H0; Apply In_1 with y; Auto.
+  Qed.
+
+  Lemma equal_mem_1: 
+    ((a:elt)(mem a s)=(mem a s')) -> (equal s s')=true.
+  Proof. 
+  Intros; Apply equal_1; Unfold Equal; Intuition; EAuto.
+  Qed.
+
+  Lemma equal_mem_2: 
+    (equal s s')=true -> (a:elt)(mem a s)=(mem a s').
+  Proof. 
+  Intros; Apply bool_1.
+  Intros; Cut (Equal s s'); [Clear H; Unfold Equal|Auto].
+  Intros H; Generalize (H a); Intuition.
+  Qed.
+
+  Lemma subset_mem_1: 
+    ((a:elt)(mem a s)=true->(mem a s')=true) -> (subset s s')=true.
+  Proof. 
+  Intros; Apply subset_1; Unfold Subset; Intuition; EAuto.
+  Qed.
+
+  Lemma subset_mem_2: 
+    (subset s s')=true -> (a:elt)(mem a s)=true -> (mem a s')=true.
+  Proof. 
+  Intros; Apply bool_1.
+  Cut (Subset s s'); [Clear H; Unfold Subset|Auto].
+  Intros H; Generalize (H a); Intuition.
+  Qed.
+  
+  Lemma empty_mem: (mem x empty)=false.
+  Proof. 
+  Apply not_true_is_false; Intro; Absurd (In x empty); Auto.
+  Qed.
+
+  Lemma is_empty_equal_empty: (is_empty s)=(equal s empty).
+  Proof. 
+  Generalize empty_1 (!is_empty_1 s) (!is_empty_2 s) 
+            (!equal_1 s empty) (!equal_2 s empty).
+  Unfold Empty Equal.
+  Case (is_empty s); Case (equal s empty); Intuition.
+  Clear H3 H1.
+  Symmetry; Apply H2; Intuition.
+  Generalize (H4 a); Intuition.
+  Generalize (H a); Intuition.
+  Clear H1 H3.
+  Apply H0; Intuition.
+  Generalize (H4 a); Intuition.
+  Generalize (H a); Intuition.
+  Qed.
+  
+  Lemma choose_mem_1: (choose s)=(Some ? x) -> (mem x s)=true.
+  Proof.  
+  Auto.
+  Qed.
+
+  Lemma choose_mem_2: (choose s)=(None ?) -> (is_empty s)=true.
+  Proof.
+  Auto.
+  Qed.
+
+  Lemma add_mem_1: (mem x (add x s))=true.
+  Proof.
+  Auto.
+  Qed.  
+ 
+  Lemma add_mem_2: 
+  ~ (E.eq x y) -> (mem y (add x s))=(mem y s).
+  Proof. 
+  Intros; Apply bool_1; Intuition; EAuto.
+  Qed.
+
+  Lemma remove_mem_1: (mem x (remove x s))=false.
+  Proof. 
+  Apply not_true_is_false; Intro; Absurd (In x (remove x s)); Auto.
+  Qed. 
+ 
+  Lemma remove_mem_2: 
+  ~ (E.eq x y) -> (mem y (remove x s))=(mem y s).
+  Proof. 
+  Intros; Apply bool_1; Intuition; EAuto. 
+  Qed.
+
+  Lemma singleton_equal_add: 
+    (equal (singleton x) (add x empty))=true.
+  Proof.
+  Apply equal_1; Unfold Equal; Intuition.
+  Apply In_1 with x; Auto.
+  Assert (E.eq a x); Auto.
+  Elim (ME.eq_dec a x); Auto.
+  Intros; Assert (In a empty). 
+  EApply add_3; EAuto.  
+  Generalize (empty_1 H0); Intuition.
+  Qed.  
+
+  Lemma union_mem: 
+    (mem x (union s s'))=(orb (mem x s) (mem x s')).
+  Proof. 
+  Apply bool_1; Intuition.
+  Elim (!union_1 s s' x); Intuition.
+  Elim (orb_prop ? ? H); Intuition.
+  Qed.
+
+  Lemma inter_mem: 
+    (mem x (inter s s'))=(andb (mem x s) (mem x s')).
+  Proof. 
+  Apply bool_1; Intuition.
+  Apply andb_true_intro; Intuition EAuto.
+  Elim (andb_prop ?? H); Intuition.
+  Qed.
+
+  Lemma diff_mem: 
+    (mem x (diff s s'))=(andb (mem x s) (negb (mem x s'))).
+  Proof. 
+  Generalize (!diff_1 s s' x) (!diff_2 s s' x) (!diff_3 s s' x).
+  LetTac s0 := (diff s s').
+  Generalize (!mem_1 s x) (!mem_1 s' x) (!mem_1 s0 x) 
+             (!mem_2 s x) (!mem_2 s' x) (!mem_2 s0 x).
+  Case (mem x s); Case (mem x s'); Case (mem x s0); Intuition.
+  Qed.
+
+  Section Cardinal.
+  
+  Lemma Add_add : 
+    (s:t)(x:elt)(Add x s (add x s)).
+  Proof.
+    Unfold Add; Intros; Intuition.
+    Elim (ME.eq_dec x0 y0); Intros; Auto.
+    Right.
+    EApply add_3; EAuto.
+    Apply In_1 with x0; Auto. 
+  Qed.
+
+  Lemma Add_remove : (s:t)(x:elt)(In x s) -> (Add x (remove x s) s). 
+  Proof. 
+    Intros; Unfold Add; Intuition.
+    Elim (ME.eq_dec x0 y0); Intros; Auto.
+    Apply In_1 with x0; Auto.
+    EAuto.
+  Qed.
+ 
+  Hints Resolve Add_add Add_remove. 
+
+  Lemma Equal_remove : (s,s':t)(x:elt)(In x s)->(Equal s s')-> 
+     (Equal (remove x s) (remove x s')).
+  Proof.
+     Unfold Equal; Intros.
+     Elim (ME.eq_dec x0 a); Intros; Auto. 
+     Split; Intros.
+     Absurd (In x0 (remove x0 s0)); Auto; Apply In_1 with a; Auto.
+     Absurd (In x0 (remove x0 s'0)); Auto; Apply In_1 with a; Auto. 
+     Elim (H0 a); Intros. 
+     Split; Intros; Apply remove_2; Auto; 
+      [Apply H1|Apply H2]; EApply remove_3;EAuto.    
+  Save.
+
+  Hints Resolve Equal_remove.
+
+  Lemma cardinal_inv_1 : (s:t)(cardinal s)=O -> (Empty s). 
+  Proof. 
+    Intros; Generalize (!choose_1 s0) (!choose_2 s0).
+    Elim (choose s0); Intuition.
+    Clear H1; Assert (In a s0); Auto.
+    Rewrite (!cardinal_2 (remove a s0) s0 a) in H; Auto.
+    Inversion H.
+  Save.
+  Hints Resolve cardinal_inv_1.
+ 
+  Lemma cardinal_inv_2 : 
+     (s:t)(n:nat)(cardinal s)=(S n) -> (EX x:elt | (In x s)).
+  Proof. 
+    Intros; Generalize (!choose_1 s0) (!choose_2 s0).
+    Elim (choose s0); Intuition. 
+    Exists a; Auto.
+    Intros; Rewrite cardinal_1 in H; Auto; Inversion H.
+  Qed.
+
+  Lemma Equal_cardinal_aux : (n:nat)(s,s':t)(cardinal s)=n -> 
+       (Equal s s')->(cardinal s)=(cardinal s').
+  Proof.
+     Induction n.
+     Intros.  
+     Rewrite H.
+     Symmetry.
+     Apply cardinal_1.
+     Generalize (cardinal_inv_1 H) H0.
+     Unfold Empty Equal; Intuition.
+     Generalize (H1 a) (H2 a); Intuition.
+     Intros.
+     Elim (cardinal_inv_2 H0); Intros.
+     Assert (In x0 s'0). 
+       Generalize (H1 x0); Intuition.  
+     Generalize H0.
+     Rewrite (!cardinal_2 (remove x0 s0) s0 x0);Auto.
+     Rewrite (!cardinal_2 (remove x0 s'0) s'0 x0); Auto.
+  Qed.
+
+  Lemma Equal_cardinal : (s,s':t)(Equal s s')->(cardinal s)=(cardinal s').
+  Proof. 
+    Intros; EApply Equal_cardinal_aux; EAuto.
+  Qed.
+
+  End Cardinal.
+
+  Hints Resolve Add_add Add_remove Equal_remove 
+                cardinal_inv_1 Equal_cardinal.
+
+  Lemma cardinal_induction : (P : t -> Prop)
+     ((s:t)(Empty s)->(P s)) -> 
+     ((s,s':t)(P s) -> (x:elt)~(In x s) -> (Add x s s') -> (P s')) -> 
+     (n:nat)(s:t)(cardinal s)=n -> (P s).
+  Proof.
+  Induction n.
+  Intros; Apply H; Auto.
+  Intros; Elim (cardinal_inv_2 H2); Intros. 
+  Apply H0 with (remove x0 s0) x0; Auto.
+  Apply H1; Auto.
+  Assert (S (cardinal (remove x0 s0))) = (S n0); Auto. 
+  Rewrite <- H2; Symmetry.
+  EApply cardinal_2; EAuto.
+  Qed.
+
+  Lemma set_induction : (P : t -> Prop)
+     ((s:t)(Empty s)->(P s)) -> 
+     ((s,s':t)(P s) -> (x:elt)~(In x s) -> (Add x s s') -> (P s')) -> 
+     (s:t)(P s).
+  Proof.
+  Intros; EApply cardinal_induction; EAuto.
+  Qed.  
+
+  Section Fold. 
+
+  Variable A:Set. 
+  Variable eqA:A->A->Prop.
+  Variable st:(Setoid_Theory ? eqA).
+  Variable i:A.
+  Variable f:elt->A->A.
+  Variable Comp:(compat_op E.eq eqA f). 
+  Variable Assoc:(transpose eqA f).
+ 
+  Lemma fold_empty: (eqA (fold f empty i) i).
+  Proof. 
+  Apply fold_1; Auto.
+  Qed.
+
+  Lemma fold_equal: 
+    (equal s s')=true -> (eqA (fold f s i) (fold f s' i)).
+  Proof. 
+     Pattern s; Apply set_induction; Intros.
+     Apply (Seq_trans ?? st) with i; Auto.
+     Apply fold_1; Auto.
+     Apply Seq_sym; Auto; Apply fold_1; Auto.
+     Apply cardinal_inv_1; Rewrite <- (Equal_cardinal (equal_2 H0)); Auto.
+     Apply (Seq_trans ?? st) with (f x0 (fold f s0 i)); Auto.
+     Apply fold_2 with eqA:=eqA; Auto.
+     Apply Seq_sym; Auto; Apply fold_2 with eqA := eqA; Auto.
+     Generalize (equal_2 H2) H1; Unfold Add Equal; Intros; 
+       Elim (H4 y0); Elim (H3 y0); Intuition.
+  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_2 with eqA:=eqA; Auto.
+    Intro; Rewrite mem_1 in H; Auto; Discriminate H. 
+  Qed.
+
+  End Fold.
+
+  Lemma cardinal_fold: (cardinal s)=(fold [_]S s O).
+  Proof. 
+    Pattern s; Apply set_induction; Intros.
+    Rewrite cardinal_1; Auto; Symmetry; Apply fold_1;Auto.
+    Rewrite (!cardinal_2 s0 s'0 x0);Auto.
+    Rewrite H; Symmetry; Change S with ([_]S x0). 
+    Apply fold_2 with eqA:=(eq nat); Auto.
+  Qed.
+
+  Section Filter.
+  
+  Variable f:elt->bool.
+  Variable Comp: (compat_bool E.eq f).
+
+  Lemma filter_mem: (mem x (filter f s))=(andb (mem x s) (f x)).
+  Proof. 
+  Apply bool_1; Intuition.
+  Apply andb_true_intro; Intuition; EAuto.
+  Elim (andb_prop ?? H); Intuition. 
+  Qed.
+
+  Lemma for_all_filter: 
+    (for_all f s)=(is_empty (filter [x](negb (f x)) s)).
+  Proof. 
+  Assert Comp' : (compat_bool E.eq [x](negb (f x))). 
+    Generalize Comp; Unfold compat_bool; Intros; Apply (f_equal ?? negb); Auto. 
+  Apply bool_1; Intuition. 
+  Apply is_empty_1.
+  Unfold Empty; Intros. 
+  Intro.
+  Assert (In a s); EAuto.
+  Generalize (filter_2 Comp' H0).
+  Generalize (for_all_2 Comp H H1); Auto.
+  Intros Eq; Rewrite Eq; Intuition.
+  Apply for_all_1; Unfold For_all; Intros; Auto. 
+  Apply bool_3.
+  Red; Intros.
+  Elim (is_empty_2 H 3!x0); Auto.
+  Qed.
+
+  Lemma exists_filter: 
+    (exists f s)=(negb (is_empty (filter f s))).
+  Proof. 
+  Apply bool_1; Intuition. 
+  Elim (exists_2 Comp H); Intuition.
+  Apply bool_6.
+  Red; Intros; Apply (is_empty_2 H0 3!x0); Auto.
+  Generalize (!choose_1 (filter f s)) (!choose_2 (filter f s)).
+  Case (choose (filter f s)).
+  Intros. 
+  Clear H1. 
+  Apply exists_1; Auto.
+  Exists e; Generalize (H0 e); Intuition; EAuto.
+  Intros. 
+  Clear H0.
+  Rewrite (!is_empty_1 (filter f s)) in H; Auto.
+  Discriminate H.
+  Qed.
+
+  Lemma partition_filter_1: 
+    (equal (fst ? ? (partition f s)) (filter f s))=true.
+  Proof. 
+  Auto.
+  Qed.
+
+  Lemma partition_filter_2: 
+    (equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s))=true.
+  Proof. 
+  Auto.
+  Qed.
+
+  End Filter.
+  End Old_Spec_Now_Properties.
+
+  Hints Immediate 
+  empty_mem   
+  is_empty_equal_empty 
+  add_mem_1
+  remove_mem_1
+  singleton_equal_add
+  union_mem
+  inter_mem
+  diff_mem 
+  cardinal_fold 
+  filter_mem
+  for_all_filter
+  exists_filter : set. 
+
+  Hints Resolve 
+  equal_mem_1
+  subset_mem_1
+  choose_mem_1
+  choose_mem_2
+  add_mem_2
+  remove_mem_2 : set.
+
+Section MoreProperties.
+
+(*s Properties of [equal] *) 
+
+Lemma equal_refl: (s:t)(equal s s)=true.
+Proof.
+Auto with set.
+Qed.
+
+Lemma equal_sym: (s,s':t)(equal s s')=(equal s' s).
+Proof.
+Intros.
+Apply bool_eq_ind;Intros.
+Rewrite equal_mem_1;Auto.
+Symmetry;Apply equal_mem_2;Auto.
+Apply (bool_eq_ind (equal s s'));Intros;Auto.
+Rewrite equal_mem_1 in H;Auto.
+Symmetry;Apply equal_mem_2;Auto.
+Qed.
+
+Lemma equal_trans: 
+ (s,u,v:t)(equal s u)=true -> (equal u v)=true -> (equal s v)=true.
+Proof.
+Intros.
+Apply equal_mem_1;Intros.
+Rewrite (equal_mem_2 H).
+Apply equal_mem_2;Assumption.
+Qed.
+
+Lemma equal_equal: 
+ (s,t_,u:t)(equal s t_)=true -> (equal s u)=(equal t_ u).
+Proof.
+Intros.
+Apply bool_eq_ind;Intros.
+Apply equal_trans with t_;Auto with set.
+Symmetry; Apply bool_eq_ind;Intros;Auto.
+Rewrite <- H0.
+Apply equal_trans with s;Auto with set.
+Rewrite equal_sym;Auto.
+Qed.
+
+Lemma equal_cardinal: 
+ (s,s':t)(equal s s')=true -> (cardinal s)=(cardinal s').
+Proof.
+Intros; Apply Equal_cardinal; Auto.
+Qed.
+
+Hints Resolve equal_refl equal_cardinal equal_equal:set.
+Hints Immediate equal_sym :set.
+
+(* Properties of [subset] *)
+
+Lemma subset_refl: (s:t)(subset s s)=true. 
+Proof.
+Auto with set.
+Qed.
+
+Lemma subset_antisym: 
+ (s,s':t)(subset s s')=true -> (subset s' s)=true -> (equal s s')=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Apply bool_eq_ind;Intros.
+EApply subset_mem_2;EAuto.
+Apply (bool_eq_ind (mem a s));Intros;Auto.
+Rewrite <- (subset_mem_2 H H2);Assumption.
+Qed.
+
+Lemma subset_trans: 
+ (s,t_,u:t)(subset s t_)=true -> (subset t_ u)=true -> (subset s u)=true.
+Proof.
+Intros.
+Apply subset_mem_1;Intros.
+Apply subset_mem_2 with t_;Intros;Auto.
+Apply subset_mem_2 with s;Auto.
+Qed.
+
+Lemma subset_equal: 
+ (s,s':t)(equal s s')=true -> (subset s s')=true.
+Proof.
+Intros.
+Apply subset_mem_1;Intros.
+Rewrite <- (equal_mem_2 H);Auto.
+Qed.
+
+Hints Resolve subset_refl subset_equal subset_antisym :set.
+
+(*s Properties of [empty] *)
+
+Lemma empty_cardinal: (cardinal empty)=O.
+Proof.
+Rewrite cardinal_fold; Auto with set.
+Apply fold_1; Auto.
+Qed.
+
+Hints Immediate empty_cardinal :set.
+
+(*s Properties of [choose] *)
+
+Lemma choose_mem_3: 
+ (s:t)(is_empty s)=false -> {x:elt|(choose s)=(Some ? x)/\(mem x s)=true}.
+Proof.
+Intros.
+Generalize (!choose_mem_1 s).
+Generalize (!choose_mem_2 s).
+Case (choose s);Intros.
+Exists e;Auto.
+LApply H0;Trivial;Intros.
+Rewrite H in H2;Discriminate H2.
+Qed.
+
+Lemma choose_mem_4: (choose empty)=(None ?).
+Proof.
+Generalize (!choose_mem_1 empty).
+Case (!choose empty);Intros;Auto.
+Absurd true=false;Auto with bool.
+Rewrite <- (H e);Auto with set.
+Qed.
+
+(*s Properties of [add] *)
+
+Lemma add_mem_3: 
+ (s:t)(x,y:elt)(mem y s)=true -> (mem y (add x s))=true.
+Proof.
+Auto.
+Qed.
+
+Lemma add_equal: 
+ (s:t)(x:elt)(mem x s)=true -> (equal (add x s) s)=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Elim (ME.eq_dec x a); Intros; Auto with set.
+Rewrite <- mem_eq with x:=x;Auto.
+Rewrite <- (mem_eq s a0);Auto.
+Rewrite H;Auto with set.
+Qed.
+
+Hints Resolve add_mem_3 add_equal :set.
+
+Lemma add_fold: 
+ (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA))
+ (f:elt->A->A)(i:A)(compat_op E.eq eqA f) -> (transpose eqA f) ->
+ (s:t)(x:elt)(mem x s)=true -> (eqA (fold f (add x s) i) (fold f s i)).
+Proof.
+Intros; Apply fold_equal with eqA:=eqA; Auto with set.
+Qed.
+
+Lemma add_cardinal_1: 
+ (s:t)(x:elt)(mem x s)=true -> (cardinal (add x s))=(cardinal s).
+Proof.
+Auto with set.
+Qed.
+
+Lemma add_cardinal_2: 
+ (s:t)(x:elt)(mem x s)=false -> (cardinal (add x s))=(S (cardinal s)).
+Proof.
+Intros.
+Do 2 Rewrite cardinal_fold.
+Change S with ([_]S x); Apply fold_add with eqA:=(eq nat); Auto.
+Qed.
+
+(*s Properties of [remove] *)
+
+Lemma remove_mem_3: 
+ (s:t)(x,y:elt)(mem y (remove x s))=true -> (mem y s)=true.
+Proof.
+Intros s x y;Elim (ME.eq_dec x y); Intro e.
+Rewrite <- mem_eq with x:=x;Auto.
+Rewrite <- (mem_eq s e);Auto.
+Rewrite (remove_mem_1 s x);Intro H;Discriminate H.
+Intros;Rewrite <- H;Symmetry;Auto with set.
+Qed.
+
+Lemma remove_equal: 
+ (s:t)(x:elt)(mem x s)=false -> (equal (remove x s) s)=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Elim (ME.eq_dec x a); Intros;Auto with set.
+Rewrite <- mem_eq with x:=x;Auto.
+Rewrite <- (mem_eq s a0);Auto;Rewrite H;Auto with set.
+Qed.
+
+Hints Resolve remove_mem_3 remove_equal :set.
+
+Lemma add_remove: 
+ (s:t)(x:elt)(mem x s)=true -> (equal (add x (remove x s)) s)=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Elim (ME.eq_dec x a); Intros;Auto with set.
+Rewrite <- mem_eq with x:=x;Auto.
+Rewrite <- (mem_eq s a0);Auto;Rewrite H;Auto with set.
+Transitivity (mem a (remove x s));Auto with set.
+Qed.
+
+Lemma remove_add: 
+ (s:t)(x:elt)(mem x s)=false -> (equal (remove x (add x s)) s)=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Elim (ME.eq_dec x a); Intros;Auto with set.
+Rewrite <- mem_eq with x:=x;Auto.
+Rewrite <- (mem_eq s a0);Auto;Rewrite H;Auto with set.
+Transitivity (mem a (add x s));Auto with set.
+Qed.
+
+Hints Immediate add_remove remove_add :set.
+
+Lemma remove_fold_1: 
+ (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA))
+ (f:elt->A->A)(i:A)(compat_op E.eq eqA f) -> (transpose eqA f) ->
+ (s:t)(x:elt)(mem x s)=true -> 
+ (eqA (f x (fold f (remove x s) i)) (fold f s i)).
+Proof.
+Intros.
+Apply Seq_sym; Auto.
+Apply fold_2 with eqA:=eqA; Auto.
+Apply Add_remove; Auto.
+Qed.
+
+Lemma remove_fold_2: 
+ (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA))
+ (f:elt->A->A)(i:A) (compat_op E.eq eqA f) -> (transpose eqA f) ->
+ (s:t)(x:elt)(mem x s)=false -> 
+ (eqA (fold f (remove x s) i) (fold f s i)).
+Proof.
+Intros.
+Apply fold_equal with eqA:=eqA; Auto with set.
+Qed.
+
+Lemma remove_cardinal_1: 
+ (s:t)(x:elt)(mem x s)=true -> (S (cardinal (remove x s)))=(cardinal s).
+Proof.
+Intros.
+Do 2 Rewrite cardinal_fold.
+Change S with ([_]S x).
+Apply remove_fold_1 with eqA:=(eq nat); Auto.
+Qed.
+
+Lemma remove_cardinal_2: 
+ (s:t)(x:elt)(mem x s)=false -> (cardinal (remove x s))=(cardinal s).
+Proof.
+Auto with set.
+Qed.
+
+(* Properties of [is_empty] *)
+
+Lemma is_empty_cardinal: (s:t)(is_empty s)=(zerob (cardinal s)).
+Proof.
+Intros.
+Apply (bool_eq_ind (is_empty s));Intros.
+Rewrite (equal_cardinal 1!s 2!empty).
+Rewrite empty_cardinal;Simpl;Trivial.
+Rewrite <- H;Symmetry;Auto with set.
+Elim (choose_mem_3 H);Intros.
+Elim p;Intros.
+Rewrite <- (remove_cardinal_1 H1).
+Simpl;Trivial.
+Qed.
+
+(*s Properties of [singleton] *)
+
+Lemma singleton_mem_1: (x:elt)(mem x (singleton x))=true.
+Proof.
+Intros.
+Rewrite (equal_mem_2 (singleton_equal_add x));Auto with set.
+Qed.
+
+Lemma singleton_mem_2: (x,y:elt)~(E.eq x y) -> (mem y (singleton x))=false.
+Proof.
+Intros.
+Rewrite (equal_mem_2 (singleton_equal_add x)).
+Rewrite <- (empty_mem y);Auto with set.
+Qed.
+
+Lemma singleton_mem_3: (x,y:elt)(mem y (singleton x))=true -> (E.eq x y).
+Proof.
+Intros.
+Elim (ME.eq_dec x y);Intros;Auto.
+Qed.
+
+Lemma singleton_cardinal: (x:elt)(cardinal (singleton x))=(S O).
+Proof.
+Intros.
+Rewrite (equal_cardinal (singleton_equal_add x)).
+Rewrite add_cardinal_2;Auto with set.
+Qed.
+
+(* General recursion principes based on [cardinal] *)
+
+Lemma cardinal_set_rec:  (P:t->Set)
+ ((s,s':t)(equal s s')=true -> (P s) -> (P s')) -> 
+ ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> 
+ (P empty) -> (n:nat)(s:t)(cardinal s)=n -> (P s).
+Proof.
+NewInduction n; Intro s; Generalize (is_empty_cardinal s); 
+  Intros eq1 eq2; Rewrite eq2 in eq1; Simpl in eq1.
+Rewrite is_empty_equal_empty in eq1.
+Rewrite equal_sym in eq1.
+Apply (H empty s eq1);Auto.
+Elim (choose_mem_3 eq1);Intros;Elim p;Clear p;Intros.
+Apply (H (add x (remove x s)) s);Auto with set.
+Apply H0;Auto with set.
+Apply IHn.
+Rewrite <- (remove_cardinal_1 H3) in eq2.
+Inversion eq2;Trivial.
+Qed.
+
+Lemma set_rec:  (P:t->Set)
+ ((s,s':t)(equal s s')=true -> (P s) -> (P s')) ->
+ ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> 
+ (P empty) -> (s:t)(P s).
+Proof.
+Intros;EApply cardinal_set_rec;EAuto.
+Qed.
+
+Lemma cardinal_set_ind:  (P:t->Prop)
+ ((s,s':t)(equal s s')=true -> (P s) -> (P s')) -> 
+ ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> 
+ (P empty) -> (n:nat)(s:t)(cardinal s)=n -> (P s).
+Proof.
+NewInduction n; Intro s; Generalize (is_empty_cardinal s); 
+  Intros eq1 eq2; Rewrite eq2 in eq1; Simpl in eq1.
+Rewrite is_empty_equal_empty in eq1.
+Rewrite equal_sym in eq1.
+Apply (H empty s eq1);Auto.
+Elim (choose_mem_3 eq1);Intros;Elim p;Clear p;Intros.
+Apply (H (add x (remove x s)) s);Auto with set.
+Apply H0;Auto with set.
+Apply IHn.
+Rewrite <- (remove_cardinal_1 H3) in eq2.
+Inversion eq2;Trivial.
+Qed.
+
+Lemma set_ind:  (P:t->Prop)
+ ((s,s':t)(equal s s')=true -> (P s) -> (P s')) ->
+ ((s:t)(x:elt)(mem x s)=false -> (P s) -> (P (add x s))) -> 
+ (P empty) -> (s:t)(P s).
+Proof.
+Intros;EApply cardinal_set_ind;EAuto.
+Qed.
+
+(*s Properties of [fold] *)
+
+Lemma fold_commutes:
+ (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory ? eqA))
+ (f:elt->A->A)(i:A)(compat_op E.eq eqA f) -> (transpose eqA f) -> (s:t)(x:elt)
+ (eqA (fold f s (f x i)) (f x (fold f s i))).
+Proof.
+Intros; Pattern s; Apply set_ind.
+Intros.
+Apply (Seq_trans ?? st) with (fold f s0 (f x i)).
+Apply fold_equal with eqA:=eqA; Auto with set.
+Rewrite equal_sym; Auto.
+Apply (Seq_trans ?? st) with (f x (fold f s0 i)); Auto.
+Apply H; Auto.
+Apply fold_equal with eqA:=eqA; Auto.
+Intros. 
+Apply (Seq_trans ?? st) with (f x0 (fold f s0 (f x i))).
+Apply fold_add with eqA:=eqA; Auto.
+Apply (Seq_trans ?? st) with (f x0 (f x (fold f s0 i))).
+Apply H; Auto.
+Apply (Seq_trans ?? st) with (f x (f x0 (fold f s0 i))).
+Apply H0; Auto.
+Apply H; Auto.
+Apply Seq_sym; Auto.
+Apply fold_add with eqA:=eqA; Auto.
+Apply (Seq_trans ?? st) with (f x i).
+Apply fold_empty; Auto.
+Apply Seq_sym; Auto.
+Apply H; Auto.
+Apply fold_empty; Auto.
+Qed.
+
+Lemma fold_plus: 
+ (s:t)(p:nat)(fold [_]S s p)=(fold [_]S s O)+p.
+Proof.
+Assert st := (gen_st nat).
+Assert fe: (compat_op E.eq (eq ?) [_:elt]S). Unfold compat_op; Auto. 
+Assert fp: (transpose (eq ?) [_:elt]S). Unfold transpose;Auto.
+Intros s p;Pattern s;Apply set_ind.
+Intros; Rewrite <- (fold_equal st p fe fp H).
+Rewrite <- (fold_equal st O fe fp H);Assumption.
+Intros.
+Assert (p:nat)(fold [_]S (add x s0) p) = (S (fold [_]S s0 p)).
+Change S with ([_]S x). 
+Intros; Apply fold_add with eqA:=(eq nat); Auto.
+Rewrite (H1 p).
+Rewrite (H1 O).
+Rewrite H0.
+Simpl; Auto.
+Intros; Do 2 Rewrite (fold_empty st);Auto.
+Qed.
+
+(*s Properties of [union] *)
+
+Lemma union_sym:
+ (s,s':t)(equal (union s s') (union s' s))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Do 2 Rewrite union_mem;Auto with bool.
+Qed.
+
+Lemma union_subset_equal: 
+ (s,s':t)(subset s s')=true->(equal (union s s') s')=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Rewrite union_mem.
+Apply (bool_eq_ind (mem a s));Intros;Simpl;Auto with set.
+Rewrite (subset_mem_2 H H0);Auto.
+Qed.
+
+Lemma union_equal_1: 
+ (s,s',s'':t)(equal s s')=true->
+ (equal (union s s'') (union s' s''))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Do 2 (Rewrite union_mem;Idtac).
+Rewrite (equal_mem_2 H a);Auto.
+Qed.
+
+Lemma union_equal_2: 
+ (s,s',s'':t)(equal s' s'')=true->
+ (equal (union s s') (union s s''))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Do 2 (Rewrite union_mem;Idtac).
+Rewrite (equal_mem_2 H a);Auto.
+Qed.
+
+Lemma union_assoc: 
+ (s,s',s'':t)
+ (equal (union (union s s') s'') (union s (union s' s'')))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Do 4 Rewrite union_mem.
+Rewrite orb_assoc;Auto.
+Qed.
+
+Lemma add_union_singleton: 
+ (s:t)(x:elt)(equal (add x s) (union (singleton x) s))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Rewrite union_mem.
+Elim (ME.eq_dec x a);Intros.
+Rewrite <- (mem_eq (add x s) a0).
+Rewrite <- (mem_eq (singleton x) a0).
+Rewrite <- (mem_eq s a0).
+Rewrite add_mem_1;Rewrite singleton_mem_1;Simpl;Auto.
+Rewrite singleton_mem_2;Simpl;Auto with set.
+Qed.
+
+Lemma union_add: 
+ (s,s':t)(x:elt)
+ (equal (union (add x s) s') (add x (union s s')))=true.
+Proof.
+Intros;Apply equal_trans with (union (union (singleton x) s) s').
+Apply union_equal_1;Apply add_union_singleton.
+Apply equal_trans with (union (singleton x) (union s s')).
+Apply union_assoc.
+Rewrite equal_sym;Apply add_union_singleton.
+Qed.
+
+(* caracterisation of [union] via [subset] *)
+
+Lemma union_subset_1:
+ (s,s':t)(subset s (union s s'))=true.
+Proof.
+Intros;Apply subset_mem_1;Intros;Rewrite union_mem;Rewrite H;Auto.
+Qed.
+
+Lemma union_subset_2:
+ (s,s':t)(subset s' (union s s'))=true.
+Proof.
+Intros;Apply subset_mem_1;Intros;Rewrite union_mem;Rewrite H;Apply orb_b_true.
+Qed.
+
+Lemma union_subset_3:
+ (s,s',s'':t)(subset s s'')=true -> (subset s' s'')=true -> 
+    (subset (union s s') s'')=true.
+Proof.
+Intros;Apply subset_mem_1;Intros;Rewrite union_mem in H1.
+Elim (orb_true_elim ? ? H1);Intros.
+Apply (subset_mem_2 H a0).
+Apply (subset_mem_2 H0 b).
+Qed.
+
+(*s Properties of [inter] *) 
+
+Lemma inter_sym:
+ (s,s':t)(equal (inter s s') (inter s' s))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Do 2 Rewrite inter_mem.
+Auto with bool.
+Qed.
+
+Lemma inter_subset_equal: 
+ (s,s':t)(subset s s')=true->(equal (inter s s') s)=true.
+Proof.
+Intros.
+Apply equal_mem_1;Intros.
+Rewrite inter_mem.
+Apply (bool_eq_ind (mem a s));Intros;Simpl;Auto.
+Rewrite (subset_mem_2 H H0);Auto.
+Qed.
+
+Lemma inter_equal_1: 
+ (s,s',s'':t)(equal s s')=true->
+ (equal (inter s s'') (inter s' s''))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Do 2 (Rewrite inter_mem;Idtac).
+Rewrite (equal_mem_2 H a);Auto.
+Qed.
+
+Lemma inter_equal_2: 
+ (s,s',s'':t)(equal s' s'')=true->
+ (equal (inter s s') (inter s s''))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Do 2 (Rewrite inter_mem;Idtac).
+Rewrite (equal_mem_2 H a);Auto.
+Qed.
+
+Lemma inter_assoc: 
+ (s,s',s'':t)
+ (equal (inter (inter s s') s'') (inter s (inter s' s'')))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Do 4 Rewrite inter_mem.
+Rewrite andb_assoc;Auto.
+Qed.
+
+Lemma union_inter_1: 
+ (s,s',s'':t)
+ (equal (inter (union s s') s'') (union (inter s s'') (inter s' s'')))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Rewrite union_mem.
+Do 3 Rewrite inter_mem.
+Rewrite union_mem. 
+Apply demorgan2.
+Qed.
+
+Lemma union_inter_2: 
+ (s,s',s'':t)
+ (equal (union (inter s s') s'') (inter (union s s'') (union s' s'')))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Rewrite union_mem.
+Do 2 Rewrite inter_mem.
+Do 2 Rewrite union_mem. 
+Apply demorgan4.
+Qed.
+
+Lemma inter_add_1: 
+ (s,s':t)(x:elt)(mem x s')=true -> 
+ (equal (inter (add x s) s') (add x (inter s s')))=true.
+Proof.
+Intros;Apply equal_trans with (inter (union (singleton x) s) s').
+Apply inter_equal_1;Apply add_union_singleton.
+Apply equal_trans with (union (inter (singleton x) s') (inter s s')).
+Apply union_inter_1.
+Apply equal_trans with (union (singleton x) (inter s s')).
+Apply union_equal_1.
+Apply inter_subset_equal.
+Apply subset_mem_1;Intros.
+Rewrite <- (mem_eq s' (singleton_mem_3 H0));Auto.
+Rewrite equal_sym;Apply add_union_singleton.
+Qed.
+
+Lemma inter_add_2: 
+ (s,s':t)(x:elt)(mem x s')=false -> 
+ (equal (inter (add x s) s') (inter s s'))=true.
+Proof.
+Intros;Apply equal_trans with (inter (union (singleton x) s) s').
+Apply inter_equal_1;Apply add_union_singleton.
+Apply equal_trans with (union (inter (singleton x) s') (inter s s')).
+Apply union_inter_1.
+Apply union_subset_equal.
+Apply subset_mem_1;Intros.
+Rewrite inter_mem in H0.
+Elim (andb_prop ? ? H0);Intros.
+Absurd (mem a s')=true;Auto.
+Rewrite <- (mem_eq s' (singleton_mem_3 H1));Auto.
+Rewrite H;Auto with bool.
+Qed.
+
+(* caracterisation of [union] via [subset] *)
+
+Lemma inter_subset_1:
+ (s,s':t)(subset (inter s s') s)=true.
+Proof.
+Intros;Apply subset_mem_1;Intros;Rewrite inter_mem in H;Elim (andb_prop ? ? H);Auto.
+Qed.
+
+Lemma inter_subset_2:
+ (s,s':t)(subset (inter s s') s')=true.
+Proof.
+Intros;Apply subset_mem_1;Intros;Rewrite inter_mem in H;Elim (andb_prop ? ? H);Auto.
+Qed.
+
+Lemma inter_subset_3:
+ (s,s',s'':t)(subset s'' s)=true -> (subset s'' s')=true -> 
+    (subset s'' (inter s s'))=true.
+Intros;Apply subset_mem_1;Intros;Rewrite inter_mem.
+Rewrite (subset_mem_2 H H1);Rewrite (subset_mem_2 H0 H1);Auto.
+Qed.
+
+(*s Properties of [union],[inter],[fold] and [cardinal] *)
+
+Lemma fold_union_inter: 
+ (A:Set)
+ (f:elt->A->A)(i:A)(compat_op E.eq (eq ?) f) -> (transpose (eq ?) f) -> 
+ (s,s':t)(fold f (union s s') (fold f (inter s s') i))
+  = (fold f s (fold f s' i)).
+Proof.
+Intro A.
+LetTac st := (gen_st A).
+Intros;Pattern s;Apply set_ind.
+Intros; Rewrite <- (fold_equal st i H H0 (inter_equal_1 s' H1)).
+Rewrite <- (fold_equal st (fold f s' i) H H0 H1).
+Rewrite <- (fold_equal st (fold f (inter s0 s') i)  H H0 (union_equal_1 s' H1));Auto.
+Intros.
+Rewrite 
+ (fold_equal st (fold f (inter (add x s0) s') i) H H0 (union_add s0 s' x)).
+Generalize (refl_equal ? (mem x s')); Pattern -1 (mem x s'); Case (mem x s');Intros.
+Rewrite (fold_equal st i H H0 (inter_add_1 s0 H3)).
+Cut (mem x (inter s0 s'))=false;Intros.
+Cut (mem x (union s0 s'))=true;Intros.
+Rewrite (fold_add st i H H0 H4).
+Rewrite (fold_commutes st);Auto.
+Rewrite (fold_equal st (fold f (inter s0 s') i) H H0 (add_equal H5)).
+Rewrite (fold_add st (fold f s' i) H H0 H1).
+Rewrite H2;Auto.
+Rewrite union_mem;Rewrite H3;Apply orb_b_true.
+Rewrite inter_mem;Rewrite H1;Simpl;Auto.
+Rewrite (fold_equal st i H H0 (inter_add_2 s0 H3)).
+Cut (mem x (union s0 s'))=false;Intros.
+Rewrite (fold_add st (fold f (inter s0 s') i) H H0 H4).
+Rewrite (fold_add st (fold f s' i) H H0 H1).
+Rewrite H2;Auto.
+Rewrite union_mem;Rewrite H3; Rewrite H1;Auto.
+Cut (subset empty s')=true;Intros.
+Rewrite (fold_equal st i H H0 (inter_subset_equal H1)).
+Do 2 Rewrite (fold_empty st);Apply fold_equal with eqA:=(eq A);Auto.
+Apply union_subset_equal;Auto.
+Apply subset_mem_1;Intros.
+Rewrite empty_mem in H1;Absurd true=false;Auto with bool.
+Qed.
+
+Lemma union_inter_cardinal: 
+ (s,s':t)(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;Auto.
+Qed.
+
+Lemma fold_union: 
+ (A:Set)(f:elt->A->A)(i:A)(compat_op E.eq (eq A) f) -> (transpose (eq A) f) -> 
+ (s,s':t)((x:elt)(andb (mem x s) (mem x s'))=false) -> 
+ (fold f (union s s') i)=(fold f s (fold f s' i)).
+Proof.
+Intros.
+Assert st:= (gen_st A).
+Rewrite <- (fold_union_inter i H H0 s s').
+Cut (equal (inter s s') empty)=true;Intros.
+Rewrite (fold_equal st i H H0 H2). 
+Rewrite (fold_empty st);Auto.
+Apply equal_mem_1;Intros.
+Rewrite inter_mem; Rewrite empty_mem;Auto.
+Qed.
+
+Lemma union_cardinal: 
+ (s,s':t)((x:elt)(andb (mem x s) (mem x s'))=false) -> 
+ (cardinal (union s s'))=(cardinal s)+(cardinal s').
+Proof.
+Intros.
+Do 3 Rewrite cardinal_fold.
+Rewrite fold_union;Auto.
+Apply fold_plus;Auto.
+Qed.
+
+(*s Properties of [diff] *)
+
+Lemma diff_subset: 
+ (s,s':t)(subset (diff s s') s)=true.
+Proof.
+Intros.
+Apply subset_mem_1;Intros.
+Rewrite diff_mem in H.
+Elim (andb_prop ? ? H);Auto.
+Qed.
+
+Lemma diff_subset_equal:
+ (s,s':t)(subset s s')=true->(equal (diff s s') empty)=true.
+Proof.
+Intros.
+Apply equal_mem_1;Intros.
+Rewrite empty_mem.
+Rewrite diff_mem.
+Generalize (!subset_mem_2 ?? H a).
+Case (mem a s);Simpl;Intros;Auto.
+Rewrite H0;Auto.
+Qed.
+
+Lemma remove_inter_singleton: 
+ (s:t)(x:elt)(equal (remove x s) (diff s (singleton x)))=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Rewrite diff_mem.
+Elim (ME.eq_dec x a); Intros.
+Rewrite <- (mem_eq (remove x s) a0).
+Rewrite <- (mem_eq s a0).
+Rewrite <- (mem_eq (singleton x) a0).
+Rewrite remove_mem_1;Rewrite singleton_mem_1;Rewrite andb_b_false;Auto.
+Rewrite singleton_mem_2;Auto;Simpl;Rewrite andb_b_true;Auto with set.
+Qed.
+
+Lemma diff_inter_empty:
+ (s,s':t)(equal (inter (diff s s') (inter s s')) empty)=true. 
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Rewrite empty_mem;Do 2 Rewrite inter_mem;Rewrite diff_mem.
+Case (mem a s);Case (mem a s');Simpl;Auto.
+Qed.
+
+Lemma diff_inter_all: 
+(s,s':t)(equal (union (diff s s') (inter s s')) s)=true.
+Proof.
+Intros;Apply equal_mem_1;Intros.
+Rewrite union_mem;Rewrite inter_mem;Rewrite diff_mem.
+Case (mem a s);Case (mem a s');Simpl;Auto.
+Qed.
+
+Lemma fold_diff_inter: 
+ (A:Set)(f:elt->A->A)(i:A)(compat_op E.eq (eq A) f) -> (transpose (eq A) f) ->
+ (s,s':t)(fold f (diff s s') (fold f (inter s s') i))=(fold f s i).
+Proof.
+Intros.
+Assert st := (gen_st A).
+Rewrite <- (fold_union_inter i H H0 (diff s s') (inter s s')).
+Rewrite (fold_equal st i H H0 (diff_inter_empty s s')).
+Rewrite (fold_empty st).
+Apply fold_equal with eqA:=(eq A);Auto.
+Apply diff_inter_all.
+Qed.
+
+Lemma diff_inter_cardinal: 
+ (s,s':t)(cardinal (diff s s'))+(cardinal (inter s s'))=(cardinal s).
+Proof.
+Intros.
+Do 3 Rewrite cardinal_fold.
+Rewrite <- fold_plus.
+Apply fold_diff_inter; Auto.
+Qed.
+
+Lemma subset_cardinal: 
+ (s,s':t)(subset s s')=true -> (le (cardinal s) (cardinal s')).
+Proof.
+Intros.
+Rewrite <- (diff_inter_cardinal s' s).
+Rewrite (equal_cardinal (inter_sym s' s)).
+Rewrite (equal_cardinal (inter_subset_equal H)); Auto with arith.
+Qed.
+
+(*s Properties of [for_all] *)
+
+Section For_all.
+
+Variable f : elt->bool.
+Variable Comp : (compat_bool E.eq f).
+
+Local Comp' : (compat_bool E.eq [x](negb (f x))).
+Proof.
+Generalize Comp; Unfold compat_bool; Intros; Apply (f_equal ?? negb);Auto.
+Qed.
+
+Lemma for_all_mem_1: 
+ (s:t)((x:elt)(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_mem; Auto.
+Rewrite empty_mem.
+Generalize (H a); Case (mem a s);Intros;Auto.
+Rewrite H0;Auto.
+Qed.
+
+Lemma for_all_mem_2: 
+ (s:t)(for_all f s)=true -> (x:elt)(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_mem; Auto.
+Rewrite empty_mem.
+Rewrite H0; Simpl;Intros.
+Replace true with (negb false);Auto;Apply negb_sym;Auto.
+Qed.
+
+Lemma for_all_mem_3: 
+ (s:t)(x:elt)(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_mem; Auto.
+Rewrite empty_mem.
+Rewrite H.
+Rewrite H0.
+Simpl;Auto.
+Qed.
+
+Lemma for_all_mem_4: 
+ (s:t)(for_all f s)=false -> {x:elt | (mem x s)=true /\ (f x)=false}.
+Intros.
+Rewrite for_all_filter in H; Auto.
+Elim (choose_mem_3 H);Intros;Elim p;Intros.
+Exists x.
+Rewrite filter_mem in H1; Auto.
+Elim (andb_prop ? ? H1).
+Split;Auto.
+Replace false with (negb true);Auto;Apply negb_sym;Auto.
+Qed.
+
+End For_all.
+
+(*s Properties of [exists] *)
+
+Section Exists.
+
+Variable f : elt->bool.
+Variable Comp : (compat_bool E.eq f).
+
+Local Comp' : (compat_bool E.eq [x](negb (f x))).
+Proof.
+Generalize Comp; Unfold compat_bool; Intros; Apply (f_equal ?? negb);Auto.
+Qed.
+
+Lemma for_all_exists: 
+ (s:t)(exists f s)=(negb (for_all [x](negb (f x)) s)).
+Proof.
+Intros.
+Rewrite for_all_filter; Auto.
+Rewrite exists_filter; Auto.
+Apply (f_equal ? ? negb).
+Do 2 Rewrite is_empty_equal_empty.
+Apply equal_equal.
+Apply equal_mem_1;Intros.
+Do 2 (Rewrite filter_mem; Auto).
+Rewrite negb_elim;Auto.
+Generalize Comp'; Unfold compat_bool; Intros; Apply (f_equal ? ?  negb); Auto.
+Qed.
+
+Lemma exists_mem_1: 
+ (s:t)((x:elt)(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: 
+ (s:t)(exists f s)=false -> (x:elt)(mem x s)=true -> (f x)=false. 
+Proof.
+Intros.
+Rewrite for_all_exists in H.
+Replace false with (negb true);Auto;Apply negb_sym;Symmetry.
+Rewrite (for_all_mem_2 1![x](negb (f x)) Comp' 3!s);Simpl;Auto.
+Replace true with (negb false);Auto;Apply negb_sym;Auto.
+Qed.
+
+Lemma exists_mem_3: 
+ (s:t)(x:elt)(mem x s)=true -> (f x)=true -> (exists f s)=true.
+Proof.
+Intros.
+Rewrite for_all_exists.
+Symmetry;Apply negb_sym;Simpl.
+Apply for_all_mem_3 with x;Auto.
+Rewrite H0;Auto.
+Qed.
+
+Lemma exists_mem_4: 
+ (s:t)(exists f s)=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
+Proof.
+Intros.
+Rewrite for_all_exists in H.
+Elim (for_all_mem_4 1![x](negb (f x)) Comp' 3!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 Exists.
+
+Section Sum.
+
+
+Definition sum := [f:elt -> nat; s:t](fold [x](plus (f x)) s 0). 
+
+Definition compat_nat := [A:Set][eqA:A->A->Prop][f:A->nat]
+ (x,x':A)(eqA x x') -> (f x)=(f x').
+Hints Unfold compat_nat.
+
+Lemma sum_plus : 
+  (f,g:elt ->nat)(compat_nat E.eq f) -> (compat_nat E.eq g) -> 
+     (s:t)(sum [x]((f x)+(g x)) s) = (sum f s)+(sum g s).
+Proof.
+Unfold sum.
+Intros f g Hf Hg.
+Assert fc : (compat_op E.eq (eq ?) [x:elt](plus (f x))).  Auto.
+Assert ft : (transpose (eq ?) [x:elt](plus (f x))). Red; Intros; Omega.
+Assert gc : (compat_op E.eq (eq ?) [x:elt](plus (g x))). Auto.
+Assert gt : (transpose (eq ?) [x:elt](plus (g x))). Red; Intros; Omega.
+Assert fgc : (compat_op E.eq (eq ?) [x:elt](plus ((f x)+(g x)))). Auto.
+Assert fgt : (transpose (eq ?) [x:elt](plus ((f x)+(g x)))). Red; Intros; Omega.
+Assert st := (gen_st nat).
+Intros s;Pattern s; Apply set_ind.
+Intros.
+Rewrite <- (fold_equal st O fc ft H).
+Rewrite <- (fold_equal st O gc gt H).
+Rewrite <- (fold_equal st O fgc fgt H); Auto.
+Assert fold_add' := [s:t; t:elt](!fold_add s t ?? st).
+Intros; Do 3 (Rewrite fold_add';Auto).
+Rewrite H0;Simpl;Omega.
+Intros; Do 3 Rewrite (fold_empty st);Auto.
+Qed.
+
+Lemma filter_equal : (f:elt -> bool)(compat_bool E.eq f) -> 
+     (s,s':t)(Equal s s') -> (Equal (filter f s) (filter f s')).
+Proof.
+Unfold Equal; Split; Intros; Elim (H0 a); Intros; Apply filter_3; EAuto.
+Qed.
+
+Lemma add_filter_1 :  (f:elt -> bool)(compat_bool E.eq f) -> 
+  (s,s':t)(x:elt) (f x)=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
+Proof.
+Unfold Add; Split; Intros; Elim (H1 y); Clear H1; Intros.
+Elim H1; [ Auto | Right; EAuto | EAuto ].
+Apply filter_3; Auto.
+Elim H2; Intros.
+Intuition.
+Apply H3; Right; EAuto.
+Elim H2; Intros.
+Rewrite <- H0; Auto.
+EAuto.
+Qed.
+
+Lemma add_filter_2 :  (f:elt -> bool)(compat_bool E.eq f) -> 
+  (s,s':t)(x:elt) (f x)=false -> (Add x s s') -> (Equal (filter f s) (filter f s')).
+Proof.
+Unfold Add Equal; Split; Intros; Elim (H1 a); Clear H1; Intros.
+Elim H1; Intros. 
+Absurd true=false; Auto with bool.
+Rewrite <- H0. 
+Rewrite <- (filter_2 H H2); Auto.
+Apply filter_3; EAuto.
+Apply H3; Right; EAuto.
+
+Elim H1; Intros. 
+Absurd true=false; Auto with bool.
+Rewrite <- H0. 
+Rewrite <- (filter_2 H H2); Auto.
+EAuto.
+EAuto.
+Qed.
+
+Lemma sum_filter : (f:elt -> bool)(compat_bool E.eq f) -> 
+  (s:t)(sum [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 fold_add' := [s:t; t:elt](!fold_add s t ?? st).
+Assert cc : (compat_op E.eq (eq ?) [x:elt](plus (if (f x) then 1 else 0))). 
+ Unfold compat_op; Intros.
+ Rewrite (Hf x x' H); Auto.
+Assert ct : (transpose (eq ?) [x:elt](plus (if (f x) then 1 else 0))).
+ Unfold transpose; Intros; Omega.
+Intros s;Pattern s; Apply set_ind.
+Intros.
+Rewrite <- (fold_equal st O  cc ct H).
+Rewrite <- (Equal_cardinal (filter_equal Hf (equal_2 H))); Auto.
+Intros; Rewrite fold_add'; 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; Intuition.
+Rewrite (cardinal_2 H1 (H4 (Add_add s0 x))); Auto.
+Rewrite <- (Equal_cardinal (H4 (Add_add s0 x))); Auto.
+Intros; Rewrite (fold_empty st);Auto.
+Rewrite cardinal_1; Auto.
+Unfold Empty; Intuition.
+Elim (!empty_1 a); EAuto.
+Qed.
+
+Lemma fold_compat : 
+  (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) -> 
+  (i:A)(s:t)((x:elt)(In x s) -> (y:A)(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_ind; Intros.
+Apply (Seq_trans ?? st) with (fold f s0 i).
+Apply fold_equal with eqA:=eqA; Auto.
+Rewrite equal_sym; Auto.
+Apply (Seq_trans ?? st) with (fold g s0 i).
+Apply H0; Intros; Apply H1; Auto.
+Elim  (equal_2 H x); Intuition.
+Apply fold_equal with eqA:=eqA; Auto.
+Apply (Seq_trans ?? st) with (f x (fold f s0 i)).
+Apply fold_add with eqA:=eqA; Auto.
+Apply (Seq_trans ?? st) with (g x (fold f s0 i)).
+Apply H1; Auto with set.
+Apply (Seq_trans ?? st) with (g x (fold g s0 i)).
+Apply gc; Auto.
+Apply Seq_sym; Auto; Apply fold_add with eqA:=eqA; Auto.
+Apply (Seq_trans ?? st) with i; [Idtac | Apply Seq_sym; Auto]; Apply fold_empty; Auto.
+Qed.
+
+Lemma sum_compat : 
+  (f,g:elt->nat)(compat_nat E.eq f) -> (compat_nat E.eq g) -> 
+  (s:t)((x:elt)(In x s) -> (f x)=(g x)) -> (sum f s)=(sum g s).
+Intros.
+Unfold sum; Apply (!fold_compat ? (eq nat)); Auto.
+Unfold transpose; Intros; Omega.
+Unfold transpose; Intros; Omega.
+Qed.
+
+End Sum.
+
+Lemma filter_orb: (f,g:elt->bool)(compat_bool E.eq f) -> (compat_bool E.eq g) ->
+  (s:t)(Equal (filter [x:elt](orb (f x) (g x)) s) (union (filter f s) (filter g s))).
+Proof.
+Intros.
+Assert (compat_bool E.eq [x](orb (f x) (g x))).
+  Unfold compat_bool; Intros.
+  Rewrite (H x y H1).
+  Rewrite (H0 x y H1); Auto.
+Unfold Equal; Split; Intros.
+Assert H3 := (filter_1 H1 H2).
+Assert H4 := (filter_2 H1 H2).
+Elim (orb_prop ?? H4); Intros; EAuto.
+Elim (union_1 H2); Intros. 
+Apply filter_3; [ Auto | EAuto | Rewrite (filter_2 H H3); Auto ].
+Apply filter_3; [ Auto | EAuto | Rewrite (filter_2 H0 H3); Auto with bool].
+Qed.
+
+End MoreProperties.
+Hints Unfold compat_nat.
+
+End Properties. 
diff --git a/theories/FSets/FSetRBT.v b/theories/FSets/FSetRBT.v
new file mode 100644
index 0000000000..c91dc719a1
--- /dev/null
+++ b/theories/FSets/FSetRBT.v
@@ -0,0 +1,2163 @@
+ (***********************************************************************)
+(*  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$ *)
+
+(** This module implements sets using red-black trees *)
+
+Require FSetInterface.
+Require FSetList.
+Require FSetBridge.
+
+Require Omega.
+Require ZArith.
+
+Import Z_scope.
+Open Scope Z_scope.
+
+Notation "[]" := (nil ?) (at level 1).
+Notation "a :: l" := (cons a l) (at level 1, l at next level).
+
+Module Make [X : OrderedType] <: Sdep with Module E := X.
+
+  Module E := X.
+  Module ME := MoreOrderedType X.
+
+  Definition elt := X.t.
+
+  (** * Red-black trees *)
+
+  Inductive color : Set := red : color | black : color.
+
+  Inductive tree : Set :=
+  | Leaf : tree
+  | Node : color -> tree -> X.t -> tree -> tree.
+
+  (** * Occurrence in a tree *)
+
+  Inductive In_tree [x:elt] : tree -> Prop :=
+  | IsRoot : (l,r:tree)(c:color)(y:elt)
+             (X.eq x y) -> (In_tree x (Node c l y r))
+  | InLeft : (l,r:tree)(c:color)(y:elt)
+             (In_tree x l) -> (In_tree x (Node c l y r))
+  | InRight : (l,r:tree)(c:color)(y:elt)
+              (In_tree x r) -> (In_tree x (Node c l y r)).
+
+  Hint In_tree := Constructors In_tree.
+
+  (** [In_tree] is  color-insensitive *)
+
+  Lemma In_color : (c,c':color)(x,y:elt)(l,r:tree)
+    (In_tree y (Node c l x r)) -> (In_tree y (Node c' l x r)).
+  Proof.
+    Inversion 1; Auto.
+  Save.
+  Hints Resolve In_color.
+
+  (** * Binary search trees *)
+
+  (** [lt_tree x s]: all elements in [s] are smaller than [x] 
+      (resp. greater for [gt_tree]) *)
+
+  Definition lt_tree [x:elt; s:tree] := (y:elt)(In_tree y s) -> (X.lt y x).
+  Definition gt_tree [x:elt; s:tree] := (y:elt)(In_tree y s) -> (X.lt x y).
+
+  Hints Unfold lt_tree gt_tree.
+
+  (** Results about [lt_tree] and [gt_tree] *)
+
+  Lemma lt_leaf : (x:elt)(lt_tree x Leaf).
+  Proof.
+    Unfold lt_tree; Intros; Inversion H.
+  Save.
+
+  Lemma gt_leaf : (x:elt)(gt_tree x Leaf).
+  Proof.
+    Unfold gt_tree; Intros; Inversion H.
+  Save.
+
+  Lemma lt_tree_node : (x,y:elt)(l,r:tree)(c:color)
+    (lt_tree x l) -> (lt_tree x r) -> (X.lt y x) -> 
+    (lt_tree x (Node c l y r)).
+  Proof.
+    Unfold lt_tree; Intuition.
+    Inversion_clear H2; Intuition.
+    Apply ME.eq_lt with y; Auto.
+  Save.
+
+  Lemma gt_tree_node : (x,y:elt)(l,r:tree)(c:color)
+    (gt_tree x l) -> (gt_tree x r) -> (E.lt x y) -> 
+    (gt_tree x (Node c l y r)).
+  Proof.
+    Unfold gt_tree; Intuition.
+    Inversion_clear H2; Intuition.
+    Apply ME.lt_eq with y; Auto.
+  Save.
+
+  Hints Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
+
+  Lemma lt_node_lt : (x,y:elt)(l,r:tree)(c:color)
+     (lt_tree x (Node c l y r)) -> (E.lt y x).
+  Proof.
+    Intros; Apply H; Auto.
+  Save.
+
+  Lemma gt_node_gt : (x,y:elt)(l,r:tree)(c:color)
+     (gt_tree x (Node c l y r)) -> (E.lt x y).
+  Proof.
+    Intros; Apply H; Auto.
+  Save.
+
+  Lemma lt_left : (x,y:elt)(l,r:tree)(c:color)
+     (lt_tree x (Node c l y r)) -> (lt_tree x l).
+  Proof.
+    Intros; Red; Intros; Apply H; Auto.
+  Save.
+
+  Lemma lt_right : (x,y:elt)(l,r:tree)(c:color)
+     (lt_tree x (Node c l y r)) -> (lt_tree x r).
+  Proof.
+    Intros; Red; Intros; Apply H; Auto.
+  Save.
+
+  Lemma gt_left : (x,y:elt)(l,r:tree)(c:color)
+     (gt_tree x (Node c l y r)) -> (gt_tree x l).
+  Proof.
+    Intros; Red; Intros; Apply H; Auto.
+  Save.
+
+  Lemma gt_right : (x,y:elt)(l,r:tree)(c:color)
+     (gt_tree x (Node c l y r)) -> (gt_tree x r).
+  Proof.
+    Intros; Red; Intros; Apply H; Auto.
+  Save.
+
+  Hints Resolve lt_node_lt gt_node_gt
+                lt_left lt_right gt_left gt_right.
+
+  Lemma lt_tree_not_in : 
+    (x:elt)(t:tree)(lt_tree x t) -> ~(In_tree x t).
+  Proof.
+    Unfold lt_tree; Intros; Red; Intros.
+    Generalize (H x H0); Intro; Absurd (X.lt x x); Auto.
+  Save.
+
+  Lemma lt_tree_trans : 
+    (x,y:elt)(X.lt x y) -> (t:tree)(lt_tree x t) -> (lt_tree y t).
+  Proof.
+    Unfold lt_tree; Ground EAuto.
+  Save.
+
+  Lemma gt_tree_not_in : 
+    (x:elt)(t:tree)(gt_tree x t) -> ~(In_tree x t).
+  Proof.
+    Unfold gt_tree; Intros; Red; Intros.
+    Generalize (H x H0); Intro; Absurd (X.lt x x); Auto.
+  Save.
+
+  Lemma gt_tree_trans : 
+    (x,y:elt)(X.lt y x) -> (t:tree)(gt_tree x t) -> (gt_tree y t).
+  Proof.
+    Unfold gt_tree; Ground EAuto.
+  Save.
+
+  Hints Resolve lt_tree_not_in lt_tree_trans 
+                gt_tree_not_in gt_tree_trans.
+
+  (** [bst t] : [t] is a binary search tree *)
+
+  Inductive bst : tree -> Prop :=
+  | BSLeaf : 
+      (bst Leaf)
+  | BSNode : (x:elt)(l,r:tree)(c:color)
+      (bst l) -> (bst r) ->
+      (lt_tree x l) -> (gt_tree x r) ->
+      (bst (Node c l x r)).
+
+  Hint bst := Constructors bst.
+
+  (** Results about [bst] *)
+ 
+  Lemma bst_left : (x:elt)(l,r:tree)(c:color)
+    (bst (Node c l x r)) -> (bst l).
+  Proof.
+    Intros x l r c H; Inversion H; Auto.
+  Save.
+
+  Lemma bst_right : (x:elt)(l,r:tree)(c:color)
+    (bst (Node c l x r)) -> (bst r).
+  Proof.
+    Intros x l r c H; Inversion H; Auto.
+  Save.
+
+  Implicits bst_left. Implicits bst_right.
+  Hints Resolve bst_left bst_right.
+
+  Lemma bst_color : (c,c':color)(x:elt)(l,r:tree)
+    (bst (Node c l x r)) -> (bst (Node c' l x r)).
+  Proof.
+    Inversion 1; Auto.
+  Save.
+  Hints Resolve bst_color.
+
+  (** Key fact about binary search trees: rotations preserve the 
+      [bst] property *)
+
+  Lemma rotate_left : (x,y:elt)(a,b,c:tree)(c1,c2,c3,c4:color)
+    (bst (Node c1 a x (Node c2 b y c))) ->
+    (bst (Node c3 (Node c4 a x b) y c)).
+  Proof.
+    Intros; Inversion H; Intuition.
+    Constructor; Intuition.
+    Constructor; EAuto.
+    EAuto.
+    Apply lt_tree_node; Intuition.
+    Apply lt_tree_trans with x; Auto.
+    Inversion H5; Auto.
+    Inversion H5; Auto.
+  Save.
+
+  Lemma rotate_right : (x,y:elt)(a,b,c:tree)(c1,c2,c3,c4:color)
+    (bst (Node c3 (Node c4 a x b) y c)) ->
+    (bst (Node c1 a x (Node c2 b y c))).
+  Proof.
+    Intros; Inversion H; Intuition.
+    Constructor; Intuition.
+    EAuto.
+    Constructor; Auto.
+    Inversion H4; Auto.
+    Inversion H4; Auto.
+    Apply gt_tree_node; Intuition.
+    Inversion H4; Auto.
+    Apply gt_tree_trans with y; Auto.
+    EAuto.
+  Save.
+
+  Hints Resolve rotate_left rotate_right.
+
+  (** * Balanced red-black trees *)
+
+  (** [rbtree n t]: [t] is a properly balanced red-black tree, i.e. it
+      satisfies the following two invariants:
+      - a red node has no red son
+      - any path from the root to a leaf has exactly [n] black nodes *)
+       
+  Definition is_not_red [t:tree] := Cases t of
+  | Leaf => True
+  | (Node black x0 x1 x2) => True
+  | (Node red x0 x1 x2) => False
+  end.
+
+  Hints Unfold is_not_red.  
+
+  Inductive rbtree : nat -> tree -> Prop :=
+  | RBLeaf : 
+      (rbtree O Leaf)
+  | RBRed : (x:elt)(l,r:tree)(n:nat)
+      (rbtree n l) -> (rbtree n r) ->
+      (is_not_red l) -> (is_not_red r) ->
+      (rbtree n (Node red l x r))
+  | RBBlack : (x:elt)(l,r:tree)(n:nat)
+      (rbtree n l) -> (rbtree n r) ->
+      (rbtree (S n) (Node black l x r)).
+
+  Hint rbtree := Constructors rbtree.
+
+  (** Results about [rbtree] *)
+
+  Lemma rbtree_left : 
+    (x:elt)(l,r:tree)(c:color)
+    (EX n:nat | (rbtree n (Node c l x r))) ->
+    (EX n:nat | (rbtree n l)).
+  Proof.
+    Intros x l r c (n,Hn); Inversion_clear Hn; Intuition EAuto.
+  Save.
+
+  Lemma rbtree_right : 
+    (x:elt)(l,r:tree)(c:color)
+    (EX n:nat | (rbtree n (Node c l x r))) ->
+    (EX n:nat | (rbtree n r)).
+  Proof.
+    Intros x l r c (n,Hn); Inversion_clear Hn; Intuition EAuto.
+  Save.
+
+  Implicits rbtree_left. Implicits rbtree_right.
+  Hints Resolve rbtree_left rbtree_right.
+
+  (** * Sets as red-black trees *)
+
+  (** A set is implement as a record [t], containing a tree, 
+      a proof that it is a binary search tree and a proof that it is 
+      a properly balanced red-black tree *)
+
+  Record t_ : Set := t_intro {
+    the_tree :> tree; 
+    is_bst : (bst the_tree);
+    is_rbtree : (EX n:nat | (rbtree n the_tree)) }.
+  Definition t := t_.
+
+  (** * Rotations *)
+
+  Lemma t_is_bst : (s:t)(bst s).
+  Proof.
+    Destruct s; Auto.
+  Save.
+  Hints Resolve t_is_bst.
+
+  (** * Logical appartness *)
+
+  Definition In : elt -> t -> Prop := [x:elt][s:t](In_tree x s).
+
+  Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
+  Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
+  Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
+  Definition Empty := [s](a:elt)~(In a s).
+  Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
+  Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
+
+  Lemma eq_In: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s).
+  Proof.
+    Unfold In; Destruct s; Simpl; Intuition Clear is_bst0 is_rbtree0.
+    Induction the_tree0; Inversion_clear H0; Intuition.
+    Apply IsRoot; EAuto.
+  Save.
+
+  Hints Resolve eq_In.
+
+  (** * Empty set *)
+
+  Definition t_empty : t.
+  Proof.
+    Exists Leaf; Auto; Exists O; Auto.
+  Defined.
+
+  Definition empty : { s:t | (x:elt)~(In x s) }. 
+  Proof.
+    Exists t_empty.
+    Unfold In; Red; Intros.
+    Inversion H.
+  Defined.
+
+  (** * Emptyness test *)
+
+  Definition is_empty : (s:t){ Empty s }+{ ~(Empty s) }.
+  Proof.
+    Unfold Empty In; Destruct s; Destruct the_tree0; Simpl; Intros.
+    Left; Auto.
+    Right; Intuition.
+    Apply (H t1); Auto.
+  Defined.
+
+  (** * Appartness *)
+
+  (** The [mem] function is deciding appartness. It exploits the [bst] property
+      to achieve logarithmic complexity. *)
+
+  Definition mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }.
+  Proof.
+    Intros x (s,Hs,Hrb).
+    Unfold In; Simpl; Clear Hrb.
+    Generalize Hs; Elim s; Simpl; Intros.
+  (* Leaf *)
+    Right. 
+    Unfold In; Red; Intros; Inversion H.
+  (* Node *)
+    Elim (X.compare x t1); Intro.
+    (* lt x t1 *)
+    Case H; Intros.
+    EAuto.
+    Left; Auto.
+    Right; Intro.
+    Inversion H1; Intuition.
+    Absurd (X.eq x t1); Auto.
+    Inversion Hs0.
+    Absurd (In_tree x t2); EAuto.
+    (* eq x t1 *)
+    Left; Auto.
+    (* lt t1 x *)
+    Case H0; Intros.
+    EAuto.
+    Left; Auto.
+    Right; Intro.
+    Inversion H1; Intuition.
+    Absurd (X.eq t1 x); Auto.
+    Inversion Hs0.
+    Absurd (In_tree x t0); EAuto.
+  Defined.
+
+  (** * Singleton set *)
+
+  Definition singleton_tree [x:elt] := (Node red Leaf x Leaf).
+
+  Lemma singleton_bst : (x:elt)(bst (singleton_tree x)).
+  Proof.
+    Unfold singleton_tree; Auto.
+  Save.
+
+  Lemma singleton_rbtree : (x:elt)(EX n:nat | (rbtree n (singleton_tree x))).
+  Proof.
+    Unfold singleton_tree; EAuto.
+  Save.
+
+  Definition singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}.
+  Proof.
+    Intro x; Exists (t_intro (singleton_tree x) (singleton_bst x)
+             (singleton_rbtree x)).
+    Unfold In singleton_tree; Simpl; Intuition.
+    Inversion_clear H; Auto; Inversion H0.
+  Defined.
+
+  (** * Insertion *)
+
+  (** [almost_rbtree n t]: [t] may have one red-red conflict at its root;
+      it satisfies [rbtree n] everywhere else *)
+
+  Inductive almost_rbtree : nat -> tree -> Prop := 
+  | ARBLeaf : 
+      (almost_rbtree O Leaf)
+  | ARBRed : (x:elt)(l,r:tree)(n:nat)
+      (rbtree n l) -> (rbtree n r) ->
+      (almost_rbtree n (Node red l x r))
+  | ARBBlack : (x:elt)(l,r:tree)(n:nat)
+      (rbtree n l) -> (rbtree n r) ->
+      (almost_rbtree (S n) (Node black l x r)).
+
+  Hint almost_rbtree := Constructors almost_rbtree.
+
+  (** Results about [almost_rbtree] *)
+
+  Lemma rbtree_almost_rbtree : 
+    (n:nat)(t:tree)(rbtree n t) -> (almost_rbtree n t).
+  Proof.
+    Destruct 1; Intuition.
+  Save.
+
+  Hints Resolve rbtree_almost_rbtree.
+
+  Lemma rbtree_almost_rbtree_ex : (s:tree)
+    (EX n:nat | (rbtree n s)) -> (EX n:nat | (almost_rbtree n s)).
+  Proof.
+    Intros s (n,Hn); Exists n; Auto.
+  Save.
+
+  Hints Resolve rbtree_almost_rbtree_ex.
+
+  Lemma almost_rbtree_rbtree_black : (x:elt)(l,r:tree)(n:nat)
+    (almost_rbtree n (Node black l x r)) -> 
+    (rbtree n (Node black l x r)).
+  Proof.
+    Inversion 1; Auto.
+  Save.
+  Hints Resolve almost_rbtree_rbtree_black.
+
+  (** Balancing functions [lbalance] and [rbalance] (see below) require
+      a rather complex pattern-matching; it is realized by the following
+      function [conflict] which returns in the sum type [Conflict] *)
+
+  Inductive Conflict [s:tree] : Set :=
+  | NoConflict : 
+      ((n:nat) (almost_rbtree n s) -> (rbtree n s)) -> 
+      (Conflict s)
+  | RedRedConflict : 
+      (a,b,c:tree)(x,y:elt)
+      (bst a) -> (bst b) -> (bst c) ->
+      (lt_tree x a) -> (gt_tree x b) -> 
+      (lt_tree y b) -> (gt_tree y c) -> (X.lt x y) ->
+      ((z:elt)(In_tree z s) <-> 
+        ((X.eq z x) \/ (X.eq z y) \/ 
+         (In_tree z a) \/ (In_tree z b) \/ (In_tree z c))) ->
+      ((n:nat)(almost_rbtree n s) ->
+              ((rbtree n a) /\ (rbtree n b) /\ (rbtree n c))) ->
+      (Conflict s).
+
+  Definition conflict : (s:tree)(bst s) -> (Conflict s).
+  Proof.
+    Destruct s; Intros.
+    (* s = Leaf *)
+    Constructor 1; Inversion 1; Auto.
+    (* s = Node c t0 t1 t2 *)
+    Induction c.
+    (* s = Node red t0 t1 t2 *)
+    Generalize H; Clear H; Case t0; Intros.
+    (* s = Node red Leaf t1 t2 *)
+    Generalize H; Clear H; Case t2; Intros.
+    (* s = Node red Leaf t1 Leaf *)
+    Constructor 1; Inversion_clear 1; Intros.
+    Constructor; Intuition.
+    (* s = Node red Leaf t1 (Node c t3 t4 t5) *)
+    Induction c.
+    (* s = Node red Leaf t1 (Node red t3 t4 t5) *)
+    Constructor 2 with a:=Leaf b:=t3 c:=t5 x:=t1 y:=t4; Intuition;
+      Solve [ Inversion_clear H; Auto; Inversion_clear H1; Auto |
+              Inversion_clear H0; Auto; Inversion_clear H2; Auto |
+              Inversion_clear H0; Auto; Inversion_clear H1; Auto |
+              Inversion_clear H1; Auto ].
+    (* s = Node red Leaf t1 (Node black t3 t4 t5) *)
+    Constructor 1; Inversion_clear 1; Intros.
+    Constructor; Intuition.
+    (* s = Node red (Node c t3 t4 t5) t1 t2 *)
+    Induction c.
+    (* s = Node red (Node red t3 t4 t5) t1 t2 *)
+    Constructor 2 with a:=t3 b:=t5 c:=t2 x:=t4 y:=t1; Intuition;
+       Solve [ Inversion_clear H; Auto; Inversion_clear H0; Auto |
+              Inversion_clear H0; Auto; Inversion_clear H1; Auto |
+              Inversion_clear H1; Auto ].
+    (* s = Node red (Node black t3 t4 t5) t1 t2 *)
+    Generalize H; Clear H; Case t2; Intros.
+    (* s = Node red (Node black t3 t4 t5) t1 Leaf *)
+    Constructor 1; Inversion_clear 1; Intros.
+    Constructor; Intuition.
+    (* s = Node red (Node black t3 t4 t5) t1 (Node c t6 t7 t8) *)
+    Induction c.
+    (* s = Node red (Node black t3 t4 t5) t1 (Node red t6 t7 t8) *)
+    Constructor 2 with a:=(Node black t3 t4 t5)
+      b:=t6 c:=t8 x:=t1 y:=t7; Intuition;
+      Solve [ Inversion_clear H; Auto; Inversion_clear H1; Auto |
+              Inversion_clear H0; Auto; Inversion_clear H2; Auto |
+              Inversion_clear H0; Auto; Inversion_clear H1; Auto |
+              Inversion_clear H1; Auto ].
+    (* s = Node red (Node black t3 t4 t5) t1 (Node black t6 t7 t8) *)
+    Constructor 1; Inversion_clear 1; Intros.
+    Constructor; Intuition.
+    (* s = Node black t0 t1 t2 *)
+    Constructor 1; Inversion_clear 1; Intros.
+    Constructor; Intuition.
+  Defined.
+
+  (** [lbalance c x l r] acts as a black node constructor,
+      solving a possible red-red conflict on [l], using the following
+      schema: 
+<<   
+     B (R (R a x b) y c) z d
+     B (R a x (R b y c)) z d -> R (B a x b) y (R c z d) 
+     B a x b -> B a x b 
+>> 
+      The result is not necessarily a black node. *)
+
+  Definition lbalance : 
+    (l:tree)(x:elt)(r:tree)
+    (lt_tree x l) -> (gt_tree x r) ->
+    (bst l) -> (bst r) ->
+    { s:tree | 
+        (bst s) /\
+        ((n:nat)((almost_rbtree n l) /\ (rbtree n r)) -> 
+                (rbtree (S n) s)) /\
+	(y:elt)(In_tree y s) <-> ((E.eq y x)\/(In_tree y l)\/(In_tree y r)) }.
+  Proof.
+    Intros; Case (conflict l).
+    Assumption.
+    (* no conflict *)
+    Exists (Node black l x r); Intuition. 
+    Inversion H3; Auto. 
+    (* red red conflict *)
+    Intros; Exists (Node red (Node black a x0 b) y
+                             (Node black c x  r)); Intuition.
+    Constructor; Intuition.
+    Constructor; Intuition.
+    Intro z; Generalize (i z); Intuition.
+    Apply lt_tree_node; Intuition.
+    Apply lt_tree_trans with x0; Auto.
+    Assert (In_tree y l). Ground. 
+    Apply gt_tree_node; Intuition.
+    Intro z; Generalize (i z); Intuition.
+    Apply X.lt_trans with x; Auto.
+    Apply H; Assumption.
+    Generalize (a0 n H4); Constructor; Intuition.
+    Generalize (i y0); Inversion_clear H3; Intuition; 
+      Inversion_clear H4; Intuition.
+    (* bug Ground *) Generalize (i y0); Intuition.
+  Defined.
+
+  (** [rbalance l x r] is similar to [lbalance], solving a possible red-red
+      conflict on [r]. The balancing schema is similar:
+<<
+     B a x (R (R b y c) z d)
+     B a x (R b y (R c z d)) -> R (B a x b) y (R c z d) 
+     B a x b -> B a x b 
+>> *)
+
+  Definition rbalance : 
+     (l:tree)(x:elt)(r:tree)
+     (lt_tree x l) -> (gt_tree x r) ->
+     (bst l) -> (bst r) ->
+     { s:tree | 
+        (bst s) /\
+        ((n:nat)((almost_rbtree n r) /\ (rbtree n l)) -> 
+                (rbtree (S n) s)) /\
+	(y:elt)(In_tree y s) <-> ((E.eq y x)\/(In_tree y l)\/(In_tree y r)) }.
+  Proof.
+    Intros; Case (conflict r).
+    Assumption.
+    (* no conflict *)
+    Exists (Node black l x r); Intuition. 
+    Inversion H3; Auto. 
+    (* red red conflict *)
+    Intros; Exists (Node red (Node black l x a) x0
+                             (Node black b y c)); Intuition.
+    Constructor; Intuition.
+    Constructor; Intuition.
+    Intro z; Generalize (i z); Intuition.
+    Assert (X.lt x x0).
+    Assert (In_tree x0 r). Ground. 
+    Apply H0; Assumption.
+    Apply lt_tree_node; Intuition.
+    Apply lt_tree_trans with x; Auto.
+    Apply gt_tree_node; Intuition.
+    Apply gt_tree_trans with y; Auto.
+    Generalize (a0 n H4); Constructor; Intuition.
+    Generalize (i y0); Inversion_clear H3; Intuition; 
+      Inversion_clear H4; Intuition.
+    (* bug Ground *) Generalize (i y0); Intuition.
+  Defined.
+
+  (** [insert x s] inserts [x] in tree [s], resulting in a possible top red-red
+      conflict when [s] is red. Its code is:
+<<  
+     insert x Empty = 
+       Node red Empty x Empty
+     insert x (Node red a y b) = 
+       if lt x y then Node red (insert x a) y b
+       else if lt y x then Node red a y (insert x b)
+       else (Node c a y b) 
+     insert x (Node black a y b) = 
+       if lt x y then lbalance (insert x a) y b
+       else if lt y x then rbalance a y (insert x b)
+       else (Node c a y b) 
+>> *)
+
+  Definition insert : 
+    (x:elt) (s:t)
+    { s':tree | (bst s') /\
+                ((n:nat)(rbtree n s) -> 
+                   ((almost_rbtree n s') /\
+                    ((is_not_red s) -> (rbtree n s')))) /\
+	        (y:elt)(In_tree y s') <-> ((E.eq y x) \/ (In_tree y s)) }.
+  Proof.
+    Intros x (s,Hs,Hrb).
+    Generalize Hs Hrb; Clear Hs Hrb; Induction s; Simpl; Intros.
+    (* Empty *)
+    Exists (singleton_tree x); Unfold singleton_tree; Simpl; Intuition.
+    Inversion H; EAuto.
+    (* Node c t0 t1 t2 *)
+    Simpl in Hrecs0 Hrecs1.
+    Induction c.
+    (* c = red => usual insertion in BST *)
+    Elim (X.compare x t0); Intro.
+    (* lt x t1 *)
+    Clear Hrecs0; Case Hrecs1; Clear Hrecs1; Intros. EAuto. EAuto.
+    Intuition.
+    Exists (Node red x0 t0 s0); Intuition.
+    Constructor; Intuition.
+    Inversion Hs; Auto.
+    Red; Intros.
+    Generalize (H2 y); Intuition.
+    Apply ME.eq_lt with x; Auto.
+    Inversion Hs; Auto.
+    Inversion Hs; Auto.
+    Inversion_clear H0; Generalize (H1 n); Intuition.  (* BUG Ground *)
+    Generalize (H2 y); Inversion H0; Intuition.
+    Generalize (H2 y); Intuition.
+    Generalize (H2 y); Inversion H3; Intuition.
+    (* eq x t1 *)
+    Clear Hrecs1 Hrecs0.
+    Exists (Node red s1 t0 s0); Intuition.
+    Apply IsRoot; EAuto.
+    (* lt t1 x *)
+    Clear Hrecs1; Case Hrecs0; Clear Hrecs0; Intros. EAuto. EAuto.
+    Intuition.
+    Exists (Node red s1 t0 x0); Intuition.
+    Constructor; Intuition.
+    Inversion Hs; Auto.
+    Inversion Hs; Auto.
+    Red; Intros.
+    Generalize (H2 y); Intuition.
+    Apply ME.lt_eq with x; Auto.
+    Inversion Hs; Auto.
+    Inversion_clear H0; (* bug Ground *) Generalize (H1 n); Intuition.
+    Generalize (H2 y); Inversion H0; Intuition.
+    Generalize (H2 y); Intuition.
+    Generalize (H2 y); Inversion H3; Intuition.
+
+    (* c = black => same code using smart constructors *)
+    Elim (X.compare x t0); Intro.
+    (* lt x t1 *)
+    Clear Hrecs0; Case Hrecs1; Clear Hrecs1; Intros. EAuto. EAuto.
+    Intuition.
+    Case (lbalance x0 t0 s0); Intuition.
+    Red; Intros.
+    Generalize (H2 y); Intuition.
+    Apply ME.eq_lt with x; Auto.
+    Inversion Hs; Auto.
+    Inversion Hs; Auto.
+    Inversion Hs; Auto.
+    Exists x1; Intuition.
+    Inversion_clear H3; Ground.
+    Inversion_clear H3; Ground.
+    Generalize (H2 y); Generalize (H5 y); Intuition.
+    Generalize (H2 y); Generalize (H5 y); Intuition.
+    Inversion H6; Generalize (H2 y); Generalize (H5 y); Intuition.
+    (* eq x t1 *)
+    Clear Hrecs1 Hrecs0.
+    Exists (Node black s1 t0 s0); Intuition.
+    Apply IsRoot; EAuto.
+    (* lt t1 x *)
+    Clear Hrecs1; Case Hrecs0; Clear Hrecs0; Intros. EAuto. EAuto.
+    Intuition.
+    Case (rbalance s1 t0 x0); Intuition.
+    Inversion Hs; Auto.
+    Red; Intros.
+    Generalize (H2 y); Intuition.
+    Apply ME.lt_eq with x; Auto.
+    Inversion Hs; Auto.
+    Inversion Hs; Auto.
+    Exists x1; Intuition.
+    Inversion_clear H3; Ground.
+    Inversion_clear H3; Ground.
+    Generalize (H2 y); Generalize (H5 y); Intuition.
+    Generalize (H2 y); Generalize (H5 y); Intuition.
+    Inversion H6; Generalize (H2 y); Generalize (H5 y); Intuition.
+  Defined.
+
+
+  (** Finally [add x s] calls [insert] and recolors the root as black:
+<<
+      add x s = match insert x s with 
+        | Node _ a y b -> Node black a y b
+        | Empty -> assert false (* absurd *)
+>> *)
+
+  Definition add : (x:elt) (s:t) { s':t | (Add x s s') }.
+  Proof.
+    Intros x s; Case (insert x s). 
+    Elim s; Clear s; Intros s Hbs Hrb;
+      Simpl; Destruct x0; Intuition.
+    (* Leaf => absurd *)
+    Absurd (In_tree x Leaf).
+    Intro; Inversion H0.
+    Ground.
+    (* Node c t0 t1 t2 *)
+    Induction c.
+    (* c = red => changed to black *)
+    LetTac s' := (Node black t0 t1 t2).
+    Assert s'bst: (bst s').
+    Unfold s'; EAuto.
+    Assert s'rbtree: (EX n:nat | (rbtree n s')).
+    Elim Hrb; Clear Hrb; Intros n Hrb.
+    Generalize (H1 n Hrb); Intuition.
+    Exists (S n); Unfold s'.
+    Inversion H3; Auto.
+    Exists (t_intro s' s'bst s'rbtree); 
+     Unfold s' Add In; Simpl.
+    Intro y; Generalize (H2 y); Clear H2; Intuition;
+      Try (Apply In_color with red; Assumption).
+    Assert (In_tree y (Node red t0 t1 t2)); Auto.
+    Apply In_color with black; Assumption.
+    (* c = black => unchanged *)
+    Assert s'rbtree: (EX n:nat | (rbtree n (Node black t0 t1 t2))).
+    Elim Hrb; Clear Hrb; Intros n Hrb.
+    Exists n; Ground. 
+    Exists (t_intro (Node black t0 t1 t2) H s'rbtree); Intuition.
+  Defined.
+
+  (** * Deletion *)
+
+  (* [UnbalancedLeft n t]: [t] is a tree of black height [S n]
+     on its left side and [n] on its right side (the root color
+     is taken into account, whathever it is) *)
+     
+  Inductive UnbalancedLeft : nat -> tree -> Prop :=
+  | ULRed : (x:elt)(l,r:tree)(n:nat)
+      (rbtree (S n) l) -> (rbtree n r) ->
+      (is_not_red l) ->
+      (UnbalancedLeft n (Node red l x r))
+  | ULBlack : (x:elt)(l,r:tree)(n:nat)
+      (rbtree (S n) l) -> (rbtree n r) ->
+      (UnbalancedLeft (S n) (Node black l x r)).
+
+  (* when a tree is unbalanced on its left, it can be repared *)
+
+  Definition unbalanced_left : 
+    (s:tree)(bst s) ->
+    { r : tree * bool | 
+        let (s',b) = r in 
+        (bst s') /\
+	((is_not_red s) /\ b=false -> (is_not_red s')) /\
+	((n:nat)(UnbalancedLeft n s) ->
+                (if b then (rbtree n s') else (rbtree (S n) s'))) /\
+        ((y:elt)(In_tree y s') <-> (In_tree y s)) }.
+  Proof.
+    Destruct s.
+    (* s = Leaf => Absurd *)
+    Intro; Exists (Leaf,false); Intuition; Inversion H0.
+    (* s = Node c t0 t1 t2 *)
+    Induction c.
+    (* s = Node red t0 t1 t2 *)
+    Destruct t0.
+    (* s = Node red Leaf t1 t2 => Absurd *)
+    Intros; Exists ((Node black Leaf t1 t2), false); Intuition.
+    Apply bst_color with red; Auto.
+    Inversion H0.
+    Inversion H5.
+    Apply In_color with black; Auto.
+    Apply In_color with red; Auto.
+    (* s = Node red (Node c0 t1 t2 t3) t4 t5 *)
+    Induction c0.
+    (* s = Node red (Node red t1 t2 t3) t4 t5 => Absurd *)
+    Intros; Exists ((Node black (Node red t1 t2 t3) t4 t5), false);
+      Intuition.
+    Apply bst_color with red; Auto.
+    Inversion H0; Elim H7.
+    Apply In_color with black; Auto.
+    Apply In_color with red; Auto.
+    (* s = Node red (Node black t1 t2 t3) t4 t5 *)
+    Intros.
+    Case (lbalance (Node red t1 t2 t3) t4 t5).
+    Inversion H; Auto.
+    Inversion H; Unfold gt_tree; Ground with In_color.
+    Inversion H; Apply bst_color with black; Auto.
+    Inversion H; Auto.
+    Intros t' Ht'; Exists (t',false); Intuition.
+    Elim H4.
+    Apply H2; Intuition.
+    Constructor; Inversion H1; Auto.
+    Inversion_clear H8; Auto.
+    Inversion_clear H8; Auto.
+    Inversion_clear H1; Auto.
+    Generalize (H3 y); Clear H3; Intuition.
+    Constructor 2; Ground with In_color.
+    Inversion_clear H1; Ground with In_color.
+    (* s = Node black t0 t1 t2 *)
+    Destruct t0.
+    (* s = Node black Leaf t1 t2 => Absurd *)
+    Intros; Exists ((Node black Leaf t1 t2), false); Intuition.
+    Inversion H0.
+    Inversion H4.
+    (* s = Node black (Node c0 t1 t2 t3) t4 t5 *)
+    Induction c0.
+    (* s = Node black (Node red t1 t2 t3) t4 t5 *)
+    Destruct t3.
+    (* s = Node black (Node red t1 t2 Leaf) t4 t5 => Absurd *)
+    Intros; Exists ((Node black (Node red t1 t2 Leaf) t4 t5), false); Intuition.
+    Inversion H0; Inversion H4; Inversion H12.
+    (* s = Node black (Node red t1 t2 (Node c1 t4 t5 t6)) t7 t8) *)
+    Induction c1.
+    (* s = Node black (Node red t1 t2 (Node red t4 t5 t6)) t7 t8) => absurd *)
+    Intros; Exists ((Node black (Node red t1 t2 (Node red t4 t5 t6)) t7 t8),false); Intuition.
+    Inversion H0; Inversion H4; Elim H14. 
+    (* s = Node black (Node red t1 t2 (Node black t4 t5 t6)) t7 t8) *)
+    Intros.
+    Case (lbalance (Node red t4 t5 t6) t7 t8).
+    Inversion H; Unfold lt_tree; Ground with In_color.
+    Inversion H; Auto.
+    Inversion H; Inversion H4; Apply bst_color with black; Auto.
+    Inversion H; Auto.
+    Intros t' Ht'; Exists ((Node black t1 t2 t'),false); Intuition.
+    Constructor; Intuition.
+    Inversion_clear H; Inversion_clear H1; Trivial.
+    Inversion_clear H; Inversion_clear H1; Trivial.
+    Intro; Generalize (H3 y); Clear H3; Intuition.
+    Apply ME.lt_eq with t7; Auto.
+    Inversion_clear H; Apply H9; Auto.
+    Inversion_clear H; Inversion_clear H5; Apply H13; Ground with In_color.
+    Inversion_clear H; Apply X.lt_trans with t7; Auto.
+    Constructor; Intuition.
+    Inversion_clear H1; Inversion_clear H4; Trivial.
+    Inversion H1.
+    Apply H2; Intuition.
+    Inversion_clear H7; Constructor; Intuition.
+    Inversion_clear H11; Trivial.
+    Inversion_clear H11; Trivial.
+    Generalize (H3 y); Clear H3; Inversion_clear H1; Intuition.
+    Ground with In_color.
+    Generalize (H3 y); Clear H3; Inversion_clear H1; Intuition.
+    Inversion_clear H3; Intuition.
+    Apply InRight; Apply H5; Apply In_color with black; Trivial.
+    (* s = Node black (Node black t1 t2 t3) t4 t5 *)
+    Intros.
+    Case (lbalance (Node red t1 t2 t3) t4 t5).
+    Inversion H; Auto.
+    Inversion H; Auto.
+    Inversion H; Apply bst_color with black; Auto.
+    Inversion H; Auto.
+    Intros t' Ht'; Exists (t',true); Intuition.
+    Discriminate H5.
+    Inversion H1.
+    Apply H2; Intuition.
+    Constructor.
+    Inversion_clear H7; Auto.
+    Inversion_clear H7; Auto.
+    Generalize (H3 y); Clear H3; Intuition.
+    Constructor 2; Ground with In_color.
+    Inversion_clear H1; Ground with In_color.
+  Defined.
+
+
+  (* [UnbalancedRight n t]: [t] is a tree of black height [S n]
+     on its right side and [n] on its left side (the root color
+     is taken into account, whathever it is) *)
+     
+  Inductive UnbalancedRight : nat -> tree -> Prop :=
+  | URRed : (x:elt)(l,r:tree)(n:nat)
+      (rbtree n l) -> (rbtree (S n) r) ->
+      (is_not_red r) ->
+      (UnbalancedRight n (Node red l x r))
+  | URBlack : (x:elt)(l,r:tree)(n:nat)
+      (rbtree n l) -> (rbtree (S n) r) ->
+      (UnbalancedRight (S n) (Node black l x r)).
+
+  (* when a tree is unbalanced on its right, it can be repared *)
+
+  Definition unbalanced_right : 
+    (s:tree)(bst s) ->
+    { r : tree * bool | 
+        let (s',b) = r in 
+        (bst s') /\
+        ((is_not_red s) /\ b=false -> (is_not_red s')) /\
+	((n:nat)(UnbalancedRight n s) ->
+                (if b then (rbtree n s') else (rbtree (S n) s'))) /\
+        ((y:elt)(In_tree y s') <-> (In_tree y s)) }.
+  Proof.
+    Destruct s.
+    (* s = Leaf => Absurd *)
+    Intro; Exists (Leaf,false); Intuition; Inversion H0.
+    (* s = Node c t0 t1 t2 *)
+    Induction c.
+    (* s = Node red t0 t1 t2 *)
+    Destruct t2.
+    (* s = Node red t0 t1 Leaf => Absurd *)
+    Intro; Exists ((Node black t0 t1 Leaf), false); Intuition.
+    Apply bst_color with red; Auto.
+    Inversion H0.
+    Inversion H6.
+    Apply In_color with black; Auto.
+    Apply In_color with red; Auto.
+    (* s = Node red t0 t1 (Node c0 t3 t4 t5) *)
+    Induction c0.
+    (* s = Node red t0 t1 (Node red t3 t4 t5) => Absurd *)
+    Intros; Exists ((Node black t0 t1 (Node red t3 t4 t5)), false);
+      Intuition.
+    Apply bst_color with red; Auto.
+    Inversion H0; Elim H7.
+    Apply In_color with black; Auto.
+    Apply In_color with red; Auto.
+    (* s = Node red t0 t1 (Node black t3 t4 t5) *)
+    Intros.
+    Case (rbalance t0 t1 (Node red t3 t4 t5)).
+    Inversion H; Auto.
+    Inversion H; Unfold gt_tree; Ground with In_color.
+    Inversion H; Auto.
+    Inversion H; Apply bst_color with black; Auto.
+    Intros t' Ht'; Exists (t',false); Intuition.
+    Elim H4.
+    Apply H2; Intuition.
+    Constructor; Inversion H1; Auto.
+    Inversion_clear H9; Auto.
+    Inversion_clear H9; Auto.
+    Inversion_clear H1; Auto.
+    Generalize (H3 y); Clear H3; Intuition.
+    Constructor 3; Ground with In_color.
+    Inversion_clear H1; Ground with In_color.
+    (* s = Node black t0 t1 t2 *)
+    Destruct t2.
+    (* s = Node black t0 t1 Leaf => Absurd *)
+    Intro; Exists ((Node black t0 t1 Leaf), false); Intuition.
+    Inversion H0.
+    Inversion H6.
+    (* s = Node black t0 t1 (Node c0 t3 t4 t5) *)
+    Induction c0.
+    (* s = Node black t0 t1 (Node red t3 t4 t5) *)
+    Destruct t3.
+    (* s = Node black t0 t1 (Node red Leaf t4 t5) => Absurd *)
+    Intros; Exists ((Node black t0 t1 (Node red Leaf t4 t5)), false); Intuition.
+    Inversion H0; Inversion H6; Inversion H10.
+    (* s = Node black t0 t1 (Node red (Node c1 t4 t5 t6) t7 t8) *)
+    Induction c1.
+    (* s = Node black t0 t1 (Node red (Node red t4 t5 t6) t7 t8) => Absurd *)
+    Intros; Exists ((Node black t0 t1 (Node red (Node red t4 t5 t6) t7 t8)),false); Intuition.
+    Inversion H0; Inversion H6; Elim H13. 
+    (* s = Node black t0 t1 (Node red (Node black t4 t5 t6) t7 t8) *)
+    Intros.
+    Case (rbalance t0 t1 (Node red t4 t5 t6)).
+    Inversion H; Auto.
+    Inversion H; Unfold gt_tree; Ground with In_color.
+    Inversion H; Auto.
+    Inversion H; Inversion H5; Apply bst_color with black; Auto.
+    Intros t' Ht'; Exists ((Node black t' t7 t8),false); Intuition.
+    Constructor; Intuition.
+    Inversion_clear H; Inversion_clear H4; Trivial.
+    Intro; Generalize (H3 y); Clear H3; Intuition.
+    Apply ME.eq_lt with t1; Auto.
+    Inversion_clear H; Apply H10; Auto.
+    Inversion_clear H; Apply X.lt_trans with t1; Auto.
+    Inversion_clear H; Inversion_clear H8; Apply H12; Ground with In_color.
+    Inversion_clear H; Inversion_clear H4; Trivial.
+    Constructor; Intuition.
+    Inversion H1.
+    Apply H2; Intuition.
+    Inversion_clear H9; Constructor; Intuition.
+    Inversion_clear H10; Trivial.
+    Inversion_clear H10; Trivial.
+    Inversion_clear H1; Inversion_clear H5; Trivial.
+    Generalize (H3 y); Clear H3; Inversion_clear H1; Intuition.
+    Ground with In_color.
+    Generalize (H3 y); Clear H3; Inversion_clear H1; Intuition.
+    Inversion_clear H3; Intuition.
+    Apply InLeft; Apply H7; Apply In_color with black; Trivial.
+    (* s = Node black t0 t1 (Node black t3 t4 t5) *)
+    Intros.
+    Case (rbalance t0 t1 (Node red t3 t4 t5)).
+    Inversion H; Auto.
+    Inversion H; Unfold gt_tree; Ground with In_color.
+    Inversion H; Auto.
+    Inversion H; Apply bst_color with black; Auto.
+    Intros t' Ht'; Exists (t',true); Intuition.
+    Discriminate H5.
+    Inversion H1.
+    Apply H2; Intuition.
+    Constructor.
+    Inversion_clear H9; Auto.
+    Inversion_clear H9; Auto.
+    Generalize (H3 y); Clear H3; Intuition.
+    Constructor 3; Ground with In_color.
+    Inversion_clear H1; Ground with In_color.
+  Defined.
+
+  Definition remove_min :
+    (s:tree)(bst s) -> ~s=Leaf ->
+    { r : tree * elt * bool |
+        let (s',r') = r in
+	let (m,b) = r' in
+        (bst s') /\
+	((is_not_red s) /\ b=false -> (is_not_red s')) /\
+        ((n:nat) (rbtree n s) -> 
+                 (if b then (lt O n) /\ (rbtree (pred n) s') else (rbtree n s'))) /\
+        ((y:elt)(In_tree y s') -> (E.lt m y)) /\
+        ((y:elt)(In_tree y s) <-> (E.eq y m) \/ (In_tree y s')) }.
+  Proof.
+    Induction s.
+    (* s = Leaf => absurd *)
+    Intuition.
+    (* s = Node c t0 t1 t2 *)
+    Destruct t0.
+    Induction c.
+    (* s = Node red Leaf t1 t2 *)
+    Intros; Clear H H0. 
+    Exists (t2,(t1,false)); Simpl; Intuition.
+    Inversion_clear H1; Auto.
+    Inversion_clear H; Auto.
+    Inversion_clear H1; Apply H5; Auto.
+    Inversion_clear H; Auto; Inversion H0.
+    (* s = Node black Leaf t1 t2 *)
+    Destruct t2; Intros; Clear H H0.
+    (* s = Node black Leaf t1 Leaf *)
+    Exists (Leaf,(t1,true)); Simpl; Intuition.
+    Inversion_clear H; Auto with arith.
+    Inversion_clear H; Auto.
+    Inversion H.
+    Inversion_clear H; Auto.
+    (* s = Node black Leaf t1 (Node c t3 t4 t5) *)
+    Exists ((Node black t3 t4 t5), (t1,false)); Intuition.
+    Inversion_clear H1; Apply bst_color with c; Auto.
+    Induction c.
+    Inversion_clear H; Inversion_clear H3; Auto.
+    Inversion_clear H; Inversion H3; Inversion H0.
+    Rewrite <- H9 in H5; Discriminate H5.
+    Inversion_clear H1; Apply H5; Apply In_color with black; Auto.
+    Inversion_clear H; Auto.
+    Inversion H0.
+    Right; Apply In_color with c; Auto.
+    Apply InRight; Apply In_color with black; Auto.
+    (* s = Node c (Node c0 t1 t2 t3) t4 t5 *)
+    Intros; Clear H0.
+    LetTac l := (Node c0 t1 t2 t3).
+    Case H; Clear H. (* remove_min l = l',m,d *)
+    Inversion H1; Auto.
+    Discriminate.
+    Destruct x; Clear x; Intro l'; Destruct p; Clear p; Intros m d.
+    Intuition. 
+    Induction d.
+    (* d = true *)
+    Case (unbalanced_right (Node c l' t4 t5)).
+    Inversion H1; Constructor; Auto.
+    Intro; Ground.
+    Destruct x; Clear x; Intros t' d'; Intuition.
+    Exists (t',(m,d')); Repeat Split.
+    Intuition.
+    Intuition.
+    Induction c; Intuition.
+    (* c = red *)
+    Assert (lt O n).
+    Unfold l in H8.
+    Induction c0; Inversion H8; Try Apply Lt.lt_O_Sn.
+    Inversion H13; Inversion H17.
+    Inversion H14; Apply Lt.lt_O_Sn.
+    Induction d'; Intuition.
+    (* d' = true *)
+    Apply H7; Clear H7.
+    Constructor; Inversion_clear H8; Auto.
+    Generalize (H0 n); Intuition.
+    Rewrite <- (Lt.S_pred n O H11); Auto.
+    (* d' = false *)
+    Rewrite (Lt.S_pred n O H11); Auto.
+    Apply H7; Clear H7.
+    Constructor; Inversion_clear H8; Auto.
+    Generalize (H0 n); Intuition.
+    Rewrite <- (Lt.S_pred n O H11); Auto.
+    (* c = black *)
+    Assert (le n (1)) \/ (lt (O) (pred n)); [ Omega | Intuition ].
+    (* n = 1 => absurd *)
+    Inversion H8.
+    Absurd (le n (1)); Auto.
+    Generalize (H0 n0 H15); Omega.
+    (* n > 1 *)
+    Induction d'; Intuition.
+    (* d' = true *)
+    Omega.
+    Apply H7; Clear H7.
+    Rewrite (Lt.S_pred (pred n) (O) H12); Auto.
+    Constructor; Inversion H8; Simpl; Auto.
+    Ground. 
+    Rewrite <- (Lt.S_pred n0 (O)); Auto. Omega.
+    (* d' = false *)
+    Rewrite (Lt.S_pred n (O)); Auto. 
+    Apply H7; Clear H7.
+    Rewrite (Lt.S_pred (pred n) (O) H12); Auto.
+    Constructor; Inversion H8; Simpl; Auto.
+    Ground. 
+    Rewrite <- (Lt.S_pred n0 (O)); Auto. Omega.
+    Omega.
+    (* ∀ y:elt,(In_tree y t') → E.lt m y *)
+    Intros y Hy; Generalize (H10 y); Clear H10; Intuition.
+    Inversion_clear H8.
+      (* y=t4 *)
+      Inversion H1.
+      Apply ME.lt_eq with t4; Auto.
+      Apply H17; Ground.
+      (* y in l' *)
+      Ground. 
+      (* y in t5 *)
+      Inversion H1.
+      Apply E.lt_trans with t4; [ Apply H17 | Apply H18]; Ground.
+    (* (In_tree y (Node c l t4 t5)) → (E.eq y m) ∨ In_tree y t' *)
+    Generalize (H10 y); Clear H10; Intuition.
+    Inversion_clear H10.
+    Ground. 
+    Generalize (H6 y); Clear H6; Intuition. 
+    Ground.
+    (* ((E.eq y m) ∨ In_tree y t') → In_tree y (Node c l t4 t5) *)
+    Intuition.
+    Ground.
+    Generalize (H10 y); Clear H10; Intuition.
+    Inversion_clear H8; Ground.
+    (* d = false *)
+    Exists ((Node c l' t4 t5),(m,false)); Simpl; Intuition.
+    Inversion_clear H1; Constructor; Auto.
+    Intro; Generalize (H6 y); Clear H6; Intuition.
+    Inversion_clear H3; Constructor; Auto.
+    Inversion_clear H3; Auto.
+    Inversion H1.
+    Apply ME.lt_eq with t4; Auto.
+    Apply H13; Ground.
+    Inversion H1.
+    Apply E.lt_trans with t4; [ Apply H13 | Apply H14 ]; Ground.
+    Generalize (H6 y); Clear H6; Intuition.
+    Inversion_clear H3; Intuition.
+    Ground.
+    Generalize (H6 y); Clear H6; Intuition.
+    Inversion_clear H7; Ground.
+  Defined.
+
+  Definition blackify :
+    (s:tree)(bst s) ->
+    { r : tree * bool | 
+        let (s',b) = r in 
+        (is_not_red s') /\ (bst s') /\
+        ((n:nat)(rbtree n s) ->
+	        if b then (rbtree n s') else (rbtree (S n) s')) /\
+        ((y:elt)(In_tree y s) <-> (In_tree y s')) }.
+  Proof.
+    Destruct s; Intros.
+    (* s = Leaf *)
+    Exists (Leaf,true); Intuition.
+    (* s = Node c t0 t1 t2 *)
+    Induction c; [ Exists ((Node black t0 t1 t2), false) 
+                 | Exists ((Node black t0 t1 t2), true) ];
+    Intuition (Try Inversion H0; Auto).
+    Apply bst_color with red; Trivial.
+  Defined.
+
+  Definition remove_aux : 
+    (x:elt)(s:tree)(bst s) ->
+    { r : tree * bool |
+        let (s',b) = r in
+        (bst s') /\
+	((is_not_red s) /\ b=false -> (is_not_red s')) /\
+        ((n:nat) (rbtree n s) -> 
+                 (if b then (lt O n) /\ (rbtree (pred n) s') else (rbtree n s'))) /\
+        ((y:elt)(In_tree y s') <-> (~(E.eq y x) /\ (In_tree y s))) }.
+  Proof.
+    Induction s.
+    (* s = Leaf *)
+    Intros; Exists (Leaf, false); Intuition.
+    Inversion H0.
+    (* s = Node c t0 t1 t2 *)
+    Intros.
+    Case (X.compare x t1); Intro.
+    (* lt x t1 *)
+    Clear H0; Case H; Clear H.
+    Inversion H1; Trivial.
+    Intros (l',d); Induction d; Intuition.
+      (* d = true => unbalanced_right *)
+      Case (unbalanced_right (Node c l' t1 t2)).
+      Constructor; Inversion_clear H1; Auto.
+      Intro; Generalize (H4 y); Intuition.
+      Intros (s',d'); Intros; Exists (s',d').
+      Intuition.
+      Clear H4 H8; Induction c.
+      Assert (UnbalancedRight (pred n) (Node red l' t1 t2)).
+      Inversion_clear H6; Generalize (H0 n); Constructor; Intuition.
+      Rewrite <- (S_pred n O); Trivial.
+      Induction d'; Intuition.
+      Inversion_clear H6; Ground.
+      Rewrite (S_pred n O); Trivial. Apply H5; Trivial.
+      Inversion_clear H6; Ground.
+      Assert (UnbalancedRight (pred n) (Node black l' t1 t2)).
+      Inversion H6; Simpl; Generalize (H0 n0); Intuition.
+      Rewrite (S_pred n0 O); Trivial.
+      Constructor; Intuition.
+      Rewrite <- (S_pred n0 O); Trivial.
+      Induction d'; Intuition.
+      Inversion_clear H6; Ground.
+      Rewrite (S_pred n O); Trivial. Apply H5; Trivial.
+      Inversion_clear H6; Ground.
+      (* In_tree y s' -> y <> x *)
+      Clear H0 H5.
+      Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H4.
+      Apply (!E.lt_not_eq x t1); Auto.
+      Apply E.eq_trans with y; Auto.
+      Intuition.
+      Apply (!ME.lt_not_gt y t1); Auto.
+      Apply ME.eq_lt with x; Trivial.
+      Inversion_clear H1; Auto.
+      (* In_tree y s' -> In_tree y (Node c t0 t1 t2)) *)
+      Clear H0 H5.
+      Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H4; Intuition.
+      (* In_tree y (Node c t0 t1 t2)) -> In_tree y s' *)
+      Clear H0 H5.
+      Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H10; Auto.
+      (* d = false => Node c l' t1 t2, false *)
+      Exists ((Node c l' t1 t2), false); Intuition.
+      Inversion_clear H1; Constructor; Intuition.
+      Intro; Intro; Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H2; Constructor; Ground.
+      Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H2; Inversion_clear H1; Intuition.
+      Apply (!E.lt_not_eq x t1); Auto.
+      Apply E.eq_trans with y; Auto.
+      Apply (!ME.lt_not_gt y t1); Auto.
+      Apply ME.eq_lt with x; Trivial.
+      Generalize (H4 y); Clear H4; Inversion_clear H2; Intuition.
+      Generalize (H4 y); Clear H4; Inversion_clear H6; Intuition.
+    (* eq x t1 *)
+    Clear H H0.
+    Generalize Dependent t2; Destruct t2; Intros.
+      (* t2 = Leaf *)
+      Induction c.
+      (* c = red => t0, false *)
+      Exists (t0, false); Intuition.
+      Inversion_clear H1; Trivial.
+      Inversion H0.
+      Inversion_clear H; Trivial.
+      Apply (!E.lt_not_eq y t1); Auto.
+      Inversion_clear H1; Apply H4; Trivial.
+      Apply E.eq_trans with x; Auto.
+      Inversion_clear H2; Intuition.
+      Absurd (X.eq y x); Auto.
+      Apply E.eq_trans with t1; Auto.
+      Inversion H.
+      (* c = black => blackify t0 *)
+      Case (blackify t0).
+      Inversion_clear H1; Trivial.
+      Intros (s',d); Intros; Exists (s',d); Intuition.
+      Inversion H3; Induction d; Intuition.
+      Generalize (H4 y); Clear H4; Inversion_clear H1; Intuition.
+      Apply (!E.lt_not_eq y t1); Auto.
+      Apply H7; Auto.
+      Apply E.eq_trans with x; Auto.
+      Ground. 
+      Generalize (H4 y); Clear H4; Inversion_clear H6; Intuition.
+      Absurd (X.eq y x); Auto.
+      Apply E.eq_trans with t1; Auto.
+      Inversion H3.
+      (* t2 = Node c0 t3 t4 t5 *)
+      Case (remove_min (Node c0 t3 t4 t5)).
+      Inversion_clear H1; Trivial.
+      Discriminate.
+      Intros (r',(m,d)); Induction d; Intuition.
+      (* d = true => unbalanced_left *)
+      Case (unbalanced_left (Node c t0 m r')).
+      Inversion_clear H1; Constructor; Trivial.
+      Intro; Intro; Apply E.lt_trans with t1.
+      Apply H7; Trivial.
+      Apply H8; Ground.
+      Intros (s',d); Intros; Exists (s',d); Intuition.
+      Clear H3 H5 H9; Induction c.
+      Assert (UnbalancedLeft (pred n) (Node red t0 m r')).
+      Inversion_clear H7; Generalize (H0 n); Constructor; Intuition.
+      Rewrite <- (S_pred n O); Trivial.
+      Induction d; Intuition.
+      Inversion_clear H7; Ground.
+      Rewrite (S_pred n O); Trivial. Apply H6; Trivial.
+      Inversion_clear H7; Ground.
+      Assert (UnbalancedLeft (pred n) (Node black t0 m r')).
+      Inversion H7; Simpl; Generalize (H0 n0); Intuition.
+      Rewrite (S_pred n0 O); Trivial.
+      Constructor; Intuition.
+      Rewrite <- (S_pred n0 O); Trivial.
+      Induction d; Intuition.
+      Inversion_clear H7; Ground.
+      Rewrite (S_pred n O); Trivial. Apply H6; Trivial.
+      Inversion_clear H7; Ground.
+      (* In_tree y s' -> y <> x *)
+      Clear H0 H6.
+      Generalize (H9 y); Clear H9; Generalize (H5 y);
+      Generalize (H3 y); Clear H3; Intuition.
+      Inversion_clear H6.
+      Apply (!E.lt_not_eq x m); Auto.
+      Inversion_clear H1.
+      Apply ME.eq_lt with t1; Trivial.
+      Apply H16; Ground.
+      Apply E.eq_trans with y; Auto.
+      Apply (!E.lt_not_eq y t1); Auto.
+      Inversion_clear H1; Apply H15; Trivial.
+      Apply E.eq_trans with x; Auto.
+      Intuition.
+      Apply (!E.lt_not_eq m y); Auto.
+      Apply (!ME.lt_not_gt t1 m); Auto.
+      Inversion_clear H1.
+      Apply H16; Ground.
+      Apply ME.lt_eq with y; Trivial.
+      Apply E.eq_trans with x; Auto.
+      (* In_tree y s' -> In_tree y (Node c t0 t1 t2)) *)
+      Clear H0 H4 H6.
+      Generalize (H9 y); Clear H9; Generalize (H5 y); Clear H5; Intuition.
+      Inversion_clear H4; Intuition.
+      (* In_tree y (Node c t0 t1 t2)) -> In_tree y s' *)
+      Clear H0 H4 H6.
+      Generalize (H9 y); Clear H9; Generalize (H5 y); Clear H5; Intuition.
+      Inversion_clear H11; Intuition.
+      Absurd (X.eq y x); Auto.
+      Apply E.eq_trans with t1; Auto.
+      (* d = false => Node c t0 m r', false *)
+      Exists ((Node c t0 m r'), false); Intuition.
+      Inversion_clear H1; Constructor; Intuition.
+      Intro; Intro; Apply E.lt_trans with t1.
+      Apply H7; Trivial.
+      Generalize (H5 m); Clear H5; Intuition.
+      Apply H8; Intuition.
+      Inversion_clear H2; Constructor; Ground.
+      Generalize (H5 y); Intuition.
+      Inversion_clear H2; Inversion_clear H1.
+      Generalize (H7 H9); Intro.
+      Apply (!E.lt_not_eq t1 y); Auto.
+      Apply H13; Trivial.
+      Apply E.eq_trans with x; Auto.
+      Apply (!E.lt_not_eq y t1); Auto.
+      Apply H12; Trivial.
+      Apply E.eq_trans with x; Auto.
+      Generalize (H10 H9); Intro.
+      Apply (!E.lt_not_eq t1 y); Auto.
+      Apply H13; Trivial.
+      Apply E.eq_trans with x; Auto.
+      Generalize (H5 y); Clear H5; Inversion_clear H2; Intuition.
+      Generalize (H5 y); Clear H5; Inversion_clear H7; Intuition.
+      Absurd (X.eq y x); Auto.
+      Apply E.eq_trans with t1; Auto.
+     (* lt t1 x *)
+    Clear H; Case H0; Clear H0.
+    Inversion H1; Trivial.
+    Intros (r',d); Induction d; Intuition.
+      (* d = true => unbalanced_left *)
+      Case (unbalanced_left (Node c t0 t1 r')).
+      Constructor; Inversion_clear H1; Auto.
+      Intro; Generalize (H4 y); Intuition.
+      Intros (s',d'); Intros; Exists (s',d').
+      Intuition.
+      Clear H4 H8; Induction c.
+      Assert (UnbalancedLeft (pred n) (Node red t0 t1 r')).
+      Inversion_clear H6; Generalize (H0 n); Constructor; Intuition.
+      Rewrite <- (S_pred n O); Trivial.
+      Induction d'; Intuition.
+      Inversion_clear H6; Ground.
+      Rewrite (S_pred n O); Trivial. Apply H5; Trivial.
+      Inversion_clear H6; Ground.
+      Assert (UnbalancedLeft (pred n) (Node black t0 t1 r')).
+      Inversion H6; Simpl; Generalize (H0 n0); Intuition.
+      Rewrite (S_pred n0 O); Trivial.
+      Constructor; Intuition.
+      Rewrite <- (S_pred n0 O); Trivial.
+      Induction d'; Intuition.
+      Inversion_clear H6; Ground.
+      Rewrite (S_pred n O); Trivial. Apply H5; Trivial.
+      Inversion_clear H6; Ground.
+      (* In_tree y s' -> y <> x *)
+      Clear H0 H5.
+      Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H4.
+      Apply (!E.lt_not_eq t1 x); Auto.
+      Apply E.eq_trans with y; Auto.
+      Apply (!ME.lt_not_gt t1 y); Auto.
+      Apply ME.lt_eq with x; Auto.
+      Inversion_clear H1; Auto.
+      Intuition.
+      (* In_tree y s' -> In_tree y (Node c t0 t1 t2)) *)
+      Clear H0 H5.
+      Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H4; Intuition.
+      (* In_tree y (Node c t0 t1 t2)) -> In_tree y s' *)
+      Clear H0 H5.
+      Generalize (H8 y); Clear H8; Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H10; Auto.
+      (* d = false => Node c t0 t1 r', false *)
+      Exists ((Node c t0 t1 r'), false); Intuition.
+      Inversion_clear H1; Constructor; Intuition.
+      Intro; Intro; Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H2; Constructor; Ground.
+      Generalize (H4 y); Clear H4; Intuition.
+      Inversion_clear H2; Inversion_clear H1; Intuition.
+      Apply (!E.lt_not_eq t1 x); Auto.
+      Apply E.eq_trans with y; Auto.
+      Apply (!ME.lt_not_gt t1 y); Auto.
+      Apply ME.lt_eq with x; Auto.
+      Generalize (H4 y); Clear H4; Inversion_clear H2; Intuition.
+      Generalize (H4 y); Clear H4; Inversion_clear H6; Intuition.
+  Defined.
+
+  Definition remove : (x:elt)(s:t)
+                      { s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}.
+  Proof.
+    Intros x (s,Hs,Hrb); Case (remove_aux x s).
+    Trivial.
+    Intros (s',b); Intuition; Clear H2.
+    Assert s'rbtree : (EX n:nat | (rbtree n s')).
+    Elim Hrb; Clear Hrb; Intros n Hn; Induction b; Ground.
+    Exists (t_intro s' H s'rbtree); Unfold In; Simpl; Intuition.
+  Defined.
+
+  (** * of_list *)
+  
+  (** Building a red-black tree from a sorted list *)
+
+  Set Implicit Arguments.
+  Record of_list_aux_Invariant [k,n:Z; l,l':(list elt); r:tree] : Prop := 
+  make_olai  
+  { olai_bst : (bst r); 
+    olai_rb : (EX kn:nat | (inject_nat kn)=k /\ (rbtree kn r)); 
+    olai_sort : (sort E.lt l'); 
+    olai_length : (Zlength l')=(Zlength l)-n; 
+    olai_same : 
+      ((x:elt)(InList E.eq x l) <-> (In_tree x r) \/ (InList E.eq x l')); 
+    olai_order : 
+      ((x,y:elt)(In_tree x r) -> (InList E.eq y l') -> (E.lt x y)) }.
+  Unset Implicit Arguments.
+
+  Lemma power_invariant :  
+    (n,k:Z)0<k ->
+    (two_p k) <= n +1 <= (two_p (Zs k)) -> 
+    let (nn,_) = (Zsplit2 (n-1)) in let (n1,n2) = nn in 
+    (two_p (Zpred k)) <= n1+1 <= (two_p k)  /\
+    (two_p (Zpred k)) <= n2+1 <= (two_p k).
+  Proof.
+    Intros.
+    Case (Zsplit2 (n-1)).
+    Intros (n1,n2) X.
+    Generalize H0; Pattern 1 k; Rewrite (Zs_pred k).
+    Rewrite two_p_S; Auto with zarith.
+    Rewrite two_p_S; Auto with zarith.
+    Apply Zlt_ZERO_pred_le_ZERO; Auto.
+  Qed.
+
+  Definition of_list_aux : 
+    (k:Z) 0<=k -> 
+    (n:Z) (two_p k) <= n+1 <= (two_p (Zs k)) -> 
+    (l:(list elt)) (sort E.lt l) -> n <= (Zlength l) -> 
+    { rl' : tree * (list elt) 
+    | let (r,l')=rl' in (of_list_aux_Invariant k n l l' r) }.
+  Proof.
+  Intros k Hk; Pattern k; Apply natlike_rec2; Try Assumption.
+  Intro n; Case (Z_eq_dec 0 n).
+  (* k=0 n=0 *)
+  Intros Hn1 Hn2 l Hl1 Hl2; Exists (Leaf, l); Intuition. 
+  Apply make_olai; Intuition.
+  Exists O; Auto.
+  Inversion H2.
+  Inversion H1.
+  (* k=0 n>0 (in fact 1) *)
+  Intros Hn1 Hn2.
+  Assert n=1. Rewrite two_p_S in Hn2; Simpl in Hn2; Auto with zarith.
+  Rewrite H.
+  Intro l; Case l.
+   (* l = [], absurd case. *)
+   Intros Hl1 Hl2; Unfold Zlength Zlt in Hl2; Elim Hl2; Trivial.
+   (* l = x::l' *)
+   Intros x l' Hl1 Hl2; Exists ((Node red Leaf x Leaf), l'); Intuition.
+   Apply make_olai; Intuition.
+   Exists O; Auto.
+   Inversion Hl1; Auto.   
+   Rewrite Zlength_cons; Auto with zarith.
+   Inversion_clear H2; Auto.
+   Inversion_clear H3; Auto; Inversion_clear H2.
+   Inversion_clear H2; Try Solve [ Inversion H4 ].
+   Inversion_clear Hl1.
+   Apply ME.In_sort with l'; Auto.
+   EApply ME.Inf_eq; EAuto.   
+  (* k>0 *)
+  Clear k Hk; Intros k Hk Hrec n Hn l Hl1 Hl2.
+  Rewrite <- Zs_pred in Hrec.
+  Generalize (power_invariant n k Hk).
+  Elim (Zsplit2 (n-1)); Intros (n1,n2) (A,B) C.  
+  Elim (C Hn); Clear C; Intros Hn1 Hn2.
+  (* First recursive call : (of_list_aux (Zpred k) n1 l) gives (lft,l') *)
+  Elim (Hrec n1 Hn1 l Hl1). 
+  Intro p; Case p; Clear p; Intros lft l'; Case l'.
+   (* l' = [], absurd case. *)
+   Intros o; ElimType False.  
+   Generalize (olai_length o).
+   Unfold 1 Zlength; Simpl; Intros X. 
+   Assert n1 = (Zlength l). Omega. Clear X.
+   Rewrite <- H in Hl2.
+   Assert n <= n2.
+     Apply Zle_trans with n1; Auto; Inversion H; Omega.
+   Assert 0<n+1.
+    Apply Zlt_le_trans with (two_p k).
+    Generalize (two_p_gt_ZERO k); Omega.
+    Inversion_clear Hn; Trivial.
+   Omega. 
+   (* l' = x :: l'' *)
+   Intros x l'' o1.
+   (* Second recursive call : (of_list_aux (Zpred k) n2 l'') gives (rht,l''') *)
+   Elim (Hrec n2 Hn2 l''); Clear Hrec.
+   Intro p; Case p; Clear p; Intros rht l''' o2.
+   Exists ((Node black lft x rht),l''').   
+   Apply make_olai.
+   (* inv1 : bst *)
+   Constructor; Try Solve [ EApply olai_bst; EAuto ].
+   Unfold lt_tree; Intros.
+   Apply (olai_order o1 7!y 8!x H); Auto.
+   Assert sorted := (olai_sort o1). 
+   Inversion_clear sorted.   
+   Unfold gt_tree; Intros.
+   Apply ME.In_sort with l''; Auto.
+   Elim (olai_same o2 y); Auto.
+   (* inv2 : rb *)  
+   Elim (inject_nat_complete k); [Intros kn; Case kn |Omega].
+   Simpl; Intros X; Rewrite X in Hk; Absurd 0<0; Auto with zarith.
+   Clear kn; Intro kn.
+   Exists (S kn); Split; Auto. 
+   Constructor.
+   Elim (olai_rb o1); Intros kn' (Hkn',Hrb); Rewrite inj_S in H.
+   Rewrite H in Hkn'; Rewrite <- Zpred_Sn in Hkn'.
+   Elim (eq_nat_dec kn kn'); Intro X; [Subst | Elim (inj_neq ?? X)]; Auto.
+   Elim (olai_rb o2); Intros kn' (Hkn',Hrb); Rewrite inj_S in H.
+   Rewrite H in Hkn'; Rewrite <- Zpred_Sn in Hkn'.
+   Elim (eq_nat_dec kn kn'); Intro X; [Subst | Elim (inj_neq ?? X)]; Auto.
+   (* inv3 : sort *)
+   Exact (olai_sort o2).
+   (* inv4 : length *)
+   Rewrite (olai_length o2).
+   Rewrite (Zpred_Sn (Zlength l'')).
+   Rewrite <- (Zlength_cons x l'').
+   Rewrite (olai_length o1); Unfold Zpred; Omega.
+   (* inv5 : same *)
+   Intro y; Generalize (olai_same o1 y); Generalize (olai_same o2 y).
+   Assert (InList E.eq y x::l'') <-> (E.eq y x) \/ (InList E.eq y l'').
+    Split; Intro H; Inversion H; Auto.
+   Generalize H; Clear H A B Hn Hn1 Hn2 o1 o2.
+   Intuition; Inversion_clear H9; Intuition.
+   (* inv6 : order *)  
+   Intros a b In_r In_l'''.
+   Inversion_clear In_r.
+   Assert sorted := (olai_sort o1).
+   Inversion_clear sorted.
+   Apply ME.eq_lt with x; Auto.
+   Apply ME.In_sort with l''; Auto.  
+   Generalize (olai_same o2 b); Intros (_,X); Auto.
+   Apply (olai_order o1 7!a 8!b); Auto.
+   Constructor 2.
+   Generalize (olai_same o2 b); Intros (_,X); Auto.
+   Apply (olai_order o2 7!a 8!b); Auto.
+  (* misc preconditions to ensure *)
+  Assert sorted := (olai_sort o1); Inversion_clear sorted; Trivial.
+  Rewrite (Zpred_Sn (Zlength l'')).
+  Rewrite <- (Zlength_cons x l'').
+  Rewrite (olai_length o1); Unfold Zpred; Omega.
+  Omega. 
+  Defined.
+
+  Definition of_list : (l:(list elt))(sort E.lt l) -> 
+    { s : t  | (x:elt)(In x s) <-> (InList E.eq x l) }. 
+  Proof.
+  Intros.
+  LetTac n := (Zlength l).
+  LetTac k := (N_digits n).
+  Assert 0<=n. 
+   Unfold n; Rewrite Zlength_correct; Auto with zarith.
+  Assert (two_p k) <= n+1 <= (two_p (Zs k)).
+    Unfold k; Generalize H0; Case n; Intros.
+    Rewrite two_p_S; Simpl; Omega.
+    Unfold N_digits; Generalize (log_inf_correct p); Omega.
+    Unfold Zle in H1; Elim H1; Auto.
+  Elim (of_list_aux k (ZERO_le_N_digits n) n H1 l); Auto.
+  Intros (r,l') o.
+  Assert (EX n : nat | (rbtree n r)).
+   Elim (olai_rb o); Intros kn Hkn; Exists kn; Intuition.
+  Exists (t_intro r (olai_bst o) H2).
+  Unfold In; Simpl.
+  Intro x; Generalize (olai_same o x).
+  Rewrite (Zlength_nil_inv l').
+  Intuition; Inversion_clear H1.
+  Rewrite (olai_length o); Unfold n; Omega.
+  Unfold n; Omega. 
+  Qed. 
+  
+  (** * Elements *)
+
+  (** [elements_tree_aux acc t] catenates the elements of [t] in infix
+      order to the list [acc] *)
+
+  Fixpoint elements_tree_aux [acc:(list X.t); t:tree] : (list X.t) :=
+    Cases t of
+    | Leaf => 
+        acc
+    | (Node _ l x r) => 
+        (elements_tree_aux (x :: (elements_tree_aux acc r)) l)
+    end.
+
+  (** then [elements_tree] is an instanciation with an empty [acc] *)
+
+  Definition elements_tree := (elements_tree_aux []).
+
+  Lemma elements_tree_aux_acc_1 : 
+    (s:tree)(acc:(list elt))
+    (x:elt)(InList E.eq x acc)->(InList E.eq x (elements_tree_aux acc s)).
+  Proof.
+    Induction s; Simpl; Intuition.
+  Save.
+  Hints Resolve elements_tree_aux_acc_1.
+
+  Lemma elements_tree_aux_1 : 
+    (s:tree)(acc:(list elt))
+    (x:elt)(In_tree x s)->(InList E.eq x (elements_tree_aux acc s)).
+  Proof.
+    Induction s; Simpl; Intuition.
+    Inversion H.
+    Inversion_clear H1; Ground.
+  Save.
+
+  Lemma elements_tree_1 : 
+    (s:tree)
+    (x:elt)(In_tree x s)->(InList E.eq x (elements_tree s)).
+  Proof.
+    Unfold elements_tree; Intros; Apply elements_tree_aux_1; Auto.
+  Save.
+  Hints Resolve elements_tree_1.
+
+  Lemma elements_tree_aux_acc_2 : 
+    (s:tree)(acc:(list elt))
+    (x:elt)(InList E.eq x (elements_tree_aux acc s)) ->
+      (InList E.eq x acc) \/ (In_tree x s).
+  Proof.
+    Induction s; Simpl; Intuition.
+    Elim (H ?? H1); Intuition.
+    Inversion_clear H2; Intuition.
+    Elim (H0 ?? H3); Intuition.
+  Save.
+  Hints Resolve elements_tree_aux_acc_2.
+
+  Lemma elements_tree_2 : 
+   (s:tree)
+    (x:elt)(InList E.eq x (elements_tree s)) -> (In_tree x s).
+  Proof.
+    Unfold elements_tree; Intros.
+    Elim (elements_tree_aux_acc_2 ??? H); Auto.
+    Intros; Inversion H0.
+  Save.
+  Hints Resolve elements_tree_2.
+
+  Lemma elements_tree_aux_sort : 
+    (s:tree)(bst s) -> (acc:(list elt))
+    (sort E.lt acc) -> 
+    ((x:elt)(InList E.eq x acc) -> (y:elt)(In_tree y s) -> (E.lt y x)) ->
+    (sort E.lt (elements_tree_aux acc s)).
+  Proof.
+    Induction s; Simpl; Intuition.
+    Apply H.
+    Inversion H1; Auto.
+    Constructor. 
+    Apply H0; Auto.
+    Inversion H1; Auto.
+    Apply ME.Inf_In_2.
+    Replace X.eq with E.eq; Replace X.lt with E.lt; Auto.
+    Intros.
+    Elim (elements_tree_aux_acc_2 t2 acc y); Intuition.
+    Inversion_clear H1.
+    Apply H9; Auto.
+    Intuition.
+    Inversion_clear H4.
+    Apply ME.lt_eq with t1; Auto.
+    Inversion_clear H1.
+    Apply H8; Auto.
+    Elim (elements_tree_aux_acc_2 ??? H6); Intuition.
+    Apply E.lt_trans with t1.
+    Inversion_clear H1; Apply H9; Auto.
+    Inversion_clear H1; Apply H10; Auto.
+  Save.
+
+  Lemma elements_tree_sort : 
+    (s:tree)(bst s) -> (sort E.lt (elements_tree s)).
+  Proof.
+    Intros; Unfold elements_tree; Apply elements_tree_aux_sort; Auto.
+    Intros; Inversion H0.
+  Save.
+  Hints Resolve elements_tree_sort.
+
+  Definition elements : 
+    (s:t){ l:(list elt) | (sort E.lt l) /\ (x:elt)(In x s)<->(InList E.eq x l)}.
+  Proof.
+    Intros (s,Hs,Hrb); Unfold In; Simpl.
+    Exists (elements_tree s); Repeat Split.
+    Apply elements_tree_sort; Auto.
+    Apply elements_tree_1; Auto.
+    Apply elements_tree_2; Auto.
+  Defined.
+
+  (** * Isomorphism with FSetList. *)
+
+  Module Lists := FSetList.Make(X).
+
+  Definition of_slist : (l:Lists.t) { s : t | (x:elt)(Lists.In x l)<->(In x s) }. 
+  Proof.
+  Intros (l,Hl).
+  Elim (of_list l Hl); Intros s Hls. 
+  Exists s; Unfold Lists.In Lists.Raw.In; Simpl; Ground.
+  Defined.
+
+  Definition to_slist : (s:t) { l : Lists.t | (x:elt)(In x s)<->(Lists.In x l) }. 
+  Proof.
+  Intro s; Elim (elements s); Intros l (Hl1, Hl2).
+  Exists (Lists.Build_slist Hl1).
+  Unfold Lists.In Lists.Raw.In; Simpl; Ground.
+  Defined.
+
+  (** * Union *)
+
+  Definition union : (s,s':t){ s'':t | (x:elt)(In x s'') <-> ((In x s)\/(In x s'))}.
+  Proof.
+  Intros s s'.
+  Elim (to_slist s); Intros l Hl.
+  Elim (to_slist s'); Intros l' Hl'.
+  Elim (of_slist (Lists.union l l')); Intros r Hr.
+  Exists r; Intuition.
+  Elim (!Lists.union_1 l l' x); Ground.
+  Elim (Hr x); Intros A _; Apply A; Apply (!Lists.union_2 l l' x); Ground.
+  Elim (Hr x); Intros A _; Apply A; Apply (!Lists.union_3 l l' x); Ground.
+  Defined.
+
+  (** * Intersection *)
+
+  Lemma inter : (s,s':t){ s'':t | (x:elt)(In x s'') <-> ((In x s)/\(In x s'))}.
+  Proof.
+  Intros s s'.
+  Elim (to_slist s); Intros l Hl.
+  Elim (to_slist s'); Intros l' Hl'.
+  Elim (of_slist (Lists.inter l l')); Intros r Hr.
+  Exists r; Intuition.
+  Elim (Hl x); Intros _ A; Apply A; Apply (!Lists.inter_1 l l' x); Ground.
+  Elim (Hl' x); Intros _ A; Apply A; Apply (!Lists.inter_2 l l' x); Ground.
+  Elim (Hr x); Intros A _; Apply A; Apply (!Lists.inter_3 l l' x); Ground.
+  Defined.
+
+  (** * Difference *)
+
+  Lemma diff : (s,s':t){ s'':t | (x:elt)(In x s'') <-> ((In x s)/\~(In x s'))}.
+  Proof.
+  Intros s s'.
+  Elim (to_slist s); Intros l Hl.
+  Elim (to_slist s'); Intros l' Hl'.
+  Elim (of_slist (Lists.diff l l')); Intros r Hr.
+  Exists r; Intuition.
+  Elim (Hl x); Intros _ A; Apply A; Apply (!Lists.diff_1 l l' x); Ground.
+  Elim (!Lists.diff_2 l l' x); Ground.  
+  Elim (Hr x); Intros A _; Apply A; Apply (!Lists.diff_3 l l' x); Ground.
+  Defined.
+
+  (** * Equality test *)
+
+  Lemma equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }.
+  Proof. 
+  Intros s s'.
+  Elim (to_slist s); Intros l Hl.
+  Elim (to_slist s'); Intros l' Hl'.
+  Assert (Lists.Equal l l')->(Lists.equal l l')=true. Exact (!Lists.equal_1 l l').
+  Assert (Lists.equal l l')=true->(Lists.Equal l l'). Exact (!Lists.equal_2 l l').
+  Generalize H H0; Case (Lists.equal l l'); Unfold Lists.Equal Equal. 
+  Left; Intros; Generalize (H2 (refl_equal ? true)); Ground.  
+  Right; Intros; Intro. 
+  Absurd false=true; [ Auto with bool | Ground ].
+  Defined.
+
+  (** * Inclusion test *)
+
+  Lemma subset : (s,s':t){ Subset s s' } + { ~(Subset s s') }.
+  Proof. 
+  Intros s s'.
+  Elim (to_slist s); Intros l Hl.
+  Elim (to_slist s'); Intros l' Hl'.
+  Assert (Lists.Subset l l')->(Lists.subset l l')=true. Exact (!Lists.subset_1 l l').
+  Assert (Lists.subset l l')=true->(Lists.Subset l l'). Exact (!Lists.subset_2 l l').
+  Generalize H H0; Case (Lists.subset l l'); Unfold Lists.Subset Subset. 
+  Left; Intros; Generalize (H2 (refl_equal ? true)); Ground.  
+  Right; Intros; Intro. 
+  Absurd false=true; [ Auto with bool | Ground ].
+  Defined.
+
+  (** * Fold *)
+
+  Fixpoint fold_tree [A:Set; f:elt->A->A; s:tree] : A -> A :=
+    Cases s of
+    | Leaf => [a]a
+    | (Node _ l x r) => [a](fold_tree A f l (f x (fold_tree A f r a)))
+    end.
+  Implicits fold_tree [1].
+
+  Definition fold_tree' := 
+   [A:Set; f:elt->A->A; s:tree] (Lists.Raw.fold f (elements_tree s)).
+  Implicits fold_tree' [1].
+
+  Lemma fold_tree_compat : (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) 
+      (s:tree)(f:elt->A->A)(compat_op E.eq eqA f) -> (a,a':A)(eqA a a') ->
+      (eqA (fold_tree f s a) (fold_tree f s a')).
+  Proof. 
+  Induction s; Simpl; Auto.
+  Qed.  
+
+  Lemma fold_tree_equiv_aux : (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) 
+     (s:tree)(f:elt->A->A)(compat_op E.eq eqA f) -> (a:A; acc : (list elt))
+     (eqA (Lists.Raw.fold f (elements_tree_aux acc s) a)
+                 (fold_tree f s (Lists.Raw.fold f acc a))).
+  Proof.
+  Induction s.
+  Simpl; Intuition.
+  Simpl; Intros.
+  EApply (Seq_trans ?? st).
+  Apply H; Auto.
+  Apply (fold_tree_compat A eqA); Simpl; Auto.
+  Qed.
+
+   Lemma fold_tree_equiv : 
+     (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) 
+     (s:tree)(f:elt->A->A; a:A)(compat_op E.eq eqA f) -> 
+     (eqA (fold_tree f s a) (fold_tree' f s a)).
+   Proof.
+   Unfold fold_tree' elements_tree. 
+   Induction s; Simpl; Auto; Intros.
+   Apply Seq_refl; Auto.
+   Apply Seq_sym; Auto.
+   EApply (Seq_trans ?? st).
+   Apply (fold_tree_equiv_aux ? eqA); Simpl; Auto.
+   Apply (fold_tree_compat ? eqA); Simpl; Auto.
+   Apply Seq_sym; Auto.
+   Qed.
+
+  Lemma fold_1 : (s:t)(A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory A eqA)) 
+    (i:A)(f:elt->A->A)(Empty s) -> (eqA (fold_tree f s i) i).
+  Proof.
+    Intros (s,Hs,Hrb); Unfold Empty Add In; Simpl; Clear Hs Hrb.
+    Case s; Simpl; Intuition.
+    Elim (H t1); Auto.
+  Save.   
+
+  Lemma fold_2 :  (s,s':t)(x:elt)
+    (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_tree f s' i) (f x (fold_tree f s i))).
+  Proof.
+  Intros (s,Hs,Hrb) (s',Hs',Hrb'); Unfold Add In; Simpl; Intros.
+  EApply (Seq_trans ?? st).
+  Apply (fold_tree_equiv ? eqA); Auto.
+  EApply (Seq_trans ?? st) with (f x (fold_tree' f s i)).
+  Unfold fold_tree'. 
+  Generalize (elements_tree_sort s Hs) (elements_tree_sort s' Hs').
+  LetTac l := (elements_tree s).
+  LetTac l' := (elements_tree s').
+  Intros Hl Hl'.
+  Apply (!Lists.Raw.fold_2 l l' Hl Hl' x A eqA) ; Auto.  
+  Unfold Lists.Raw.Add l l'; Split; Intros; Elim (H2 y);  Intuition; Elim H4; Auto.
+  Apply (Seq_sym ?? st).
+  Apply H; Auto.
+  Apply (fold_tree_equiv ? eqA); Auto.
+  Qed.
+
+  Definition fold : 
+   (A:Set)
+   (f:elt->A->A) 
+   { fold:t -> A -> A | (s,s':t)(a:A)
+      (eqA:A->A->Prop)(st:(Setoid_Theory A eqA))
+      ((Empty s) -> (eqA (fold s a) a)) /\
+      ((compat_op E.eq eqA f)->(transpose eqA f) ->
+        (x:elt) (Add x s s') -> ~(In x s) -> (eqA (fold s' a) (f x (fold s a)))) }.  
+  Proof.
+    Intros A f; Exists [s:t](fold_tree f s); Split; Intros.
+    Apply fold_1; Auto.
+    Apply (fold_2 s s' x A eqA); Auto.
+  Defined.
+
+  (** * Cardinal *)
+
+  Definition cardinal : 
+    {cardinal : t -> nat | (s,s':t)
+       ((Empty s) -> (cardinal s)=O) /\
+       ((x:elt) (Add x s s') -> ~(In x s) -> (cardinal s')=(S (cardinal s)))}.
+  Proof.
+    Assert st : (Setoid_Theory ? (eq nat)).
+     Constructor; Auto; Intros; EApply trans_eq; EAuto.
+    Elim (fold nat [_]S); Intro f; Exists [s:t](f s O); Split; Intros.
+    Elim (p s s O ? st); Auto.
+    Elim (p s s' O ? st); Intros; EApply H2; EAuto.
+  Qed.
+
+  (** * Filter *)
+
+  Module DLists := DepOfNodep(Lists).
+
+  Definition filter : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { s':t | (compat_P E.eq P) -> (x:elt)(In x s') <-> ((In x s)/\(P x)) }.
+  Proof.
+  Intros.
+  Elim (to_slist s); Intros l Hl.
+  Elim (DLists.filter Pdec l); Intros l' Hl'.
+  Elim (of_slist l'); Intros r Hr.
+  Exists r.
+  Intros C; Generalize (Hl' C); Ground.
+  Qed.
+
+  Lemma for_all : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { (compat_P E.eq P) -> (For_all P s) } + 
+     { (compat_P E.eq P) -> ~(For_all P s) }.
+  Proof.
+  Intros; Unfold For_all.
+  Elim (to_slist s); Intros l Hl.
+  Elim (DLists.for_all Pdec l); Unfold Lists.For_all; Intro H; [Left|Right]; 
+    Intro C; Generalize (H C); Ground.
+  Qed.
+
+  Lemma exists : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { (compat_P E.eq P) -> (Exists P s) } + 
+     { (compat_P E.eq P) -> ~(Exists P s) }.
+  Proof.
+  Intros; Unfold Exists.
+  Elim (to_slist s); Intros l Hl.
+  Elim (DLists.exists Pdec l); Unfold Lists.Exists; Intro H; [Left|Right]; 
+    Intro C; Generalize (H C); Ground.
+  Qed.
+
+  Lemma partition : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
+     { partition : t*t | 
+        let (s1,s2) = partition in 
+	(compat_P E.eq P) -> 
+	((For_all P s1) /\ 
+	 (For_all ([x]~(P x)) s2) /\
+	 (x:elt)(In x s)<->((In x s1)\/(In x s2))) }.
+  Proof.
+  Intros; Unfold For_all.
+  Elim (to_slist s); Intros l Hl.
+  Elim (DLists.partition Pdec l); Unfold Lists.For_all; Intros (l1,l2) H.
+  Elim (of_slist l1); Intros s1 Hs1.
+  Elim (of_slist l2); Intros s2 Hs2.
+  Exists (s1,s2).
+  Intro Comp; Elim (H Comp); Intros A (B,C); Clear H Comp.
+  Intuition.
+  Apply A; Ground.
+  Apply (B x); Ground.
+  Elim (C x); Intros D _; Elim D; [Left|Right|Idtac]; Ground.
+  Ground.
+  Ground.
+  Qed.
+
+  (** * Minimum element *)
+
+  Definition min_elt : 
+     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }.
+  Proof.
+    Intros (s,Hs,Hrb).
+    Unfold For_all Empty In; Simpl.
+    Generalize Hs; Clear Hs Hrb; Induction s; Simpl; Intros.
+    (* s = Leaf *)
+    Right; Intros; Intro; Inversion H.
+    (* s = Node c s1 t0 s0 *)
+    Clear Hrecs0; Generalize Hs Hrecs1; Clear Hs Hrecs1; Case s1; Intros.
+    (* s1 = Leaf *)
+    Left; Exists t0; Intuition.
+    Inversion_clear H.
+    Absurd (X.eq x t0); Auto.
+    Inversion H1.
+    Inversion_clear Hs; Absurd (E.lt x t0); Auto.
+    (* s1 = Node c0 t1 t2 t3 *)
+    Case Hrecs1; Clear Hrecs1.
+    Inversion Hs; Auto.
+    (* a minimum for [s1] *)
+    Intros (m,Hm); Left; Exists m; Intuition.
+    Apply (H0 x); Auto.
+    Assert (X.lt m t0).
+    Inversion_clear Hs; Auto.
+    Inversion_clear H1; Auto.
+    Elim (!X.lt_not_eq x t0); [ EAuto | Auto ].
+    Inversion_clear Hs.
+    Elim (!ME.lt_not_gt x t0); [ EAuto | Auto ].
+    (* non minimum for [s1] => absurd *)
+    Intro; Right; Intuition.
+    Apply (n t2); Auto.
+  Defined.
+
+  (** * Maximum element *)
+
+  Definition max_elt : 
+     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }.
+   Proof.
+    Intros (s,Hs,Hrb).
+    Unfold For_all Empty In; Simpl.
+    Generalize Hs; Clear Hs Hrb; Induction s; Simpl; Intros.
+    (* s = Leaf *)
+    Right; Intros; Intro; Inversion H.
+    (* s = Node c s1 t0 s0 *)
+    Clear Hrecs1; Generalize Hs Hrecs0; Clear Hs Hrecs0; Case s0; Intros.
+    (* s0 = Leaf *)
+    Left; Exists t0; Intuition.
+    Inversion_clear H.
+    Absurd (X.eq x t0); Auto.
+    Inversion_clear Hs; Absurd (E.lt t0 x); Auto.
+    Inversion H1.
+    (* s0 = Node c0 t1 t2 t3 *)
+    Case Hrecs0; Clear Hrecs0.
+    Inversion Hs; Auto.
+    (* a maximum for [s0] *)
+    Intros (m,Hm); Left; Exists m; Intuition.
+    Apply (H0 x); Auto.
+    Assert (X.lt t0 m).
+    Inversion_clear Hs; Auto.
+    Inversion_clear H1; Auto.
+    Elim (!X.lt_not_eq x t0); [ EAuto | Auto ].
+    Inversion_clear Hs.
+    Elim (!ME.lt_not_gt t0 x); [ EAuto | Auto ].
+    (* non maximum for [s0] => absurd *)
+    Intro; Right; Intuition.
+    Apply (n t2); Auto.
+  Defined.
+
+  (** * Any element *)
+
+  Definition choose : (s:t) { x:elt | (In x s)} + { Empty s }.
+  Proof.
+    Intros (s,Hs,Hrb); Unfold Empty In; Simpl; Case s; Intuition.
+    Right; Intros; Inversion H.
+    Left; Exists t1; Auto.
+  Defined.
+
+  (** * Comparison *)
+  
+  Definition eq : t -> t -> Prop := Equal.
+
+  Definition lt : t -> t -> Prop :=
+    [s,s':t]let (l,_) = (to_slist s) in
+            let (l',_) = (to_slist s') in
+	    (Lists.lt l l').
+
+  Lemma eq_refl: (s:t)(eq s s). 
+  Proof.
+    Unfold eq Equal; Intuition.
+  Save.
+
+  Lemma eq_sym: (s,s':t)(eq s s') -> (eq s' s).
+  Proof.
+    Unfold eq Equal; Ground.
+  Save.
+
+  Lemma eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s'').
+  Proof.
+    Unfold eq Equal; Ground.
+  Save.
+
+  Lemma lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s'').
+  Proof.
+    Intros s s' s''; Unfold lt.
+    Elim (to_slist s); Intros l Hl.
+    Elim (to_slist s'); Intros l' Hl'.
+    Elim (to_slist s''); Intros l'' Hl''.
+    Exact (!Lists.lt_trans l l' l'').
+  Save.
+
+  Definition eql : t -> t -> Prop :=
+    [s,s':t]let (l,_) = (to_slist s) in
+            let (l',_) = (to_slist s') in
+	    (Lists.eq l l').
+
+  Lemma eq_eql : (s,s':t)(eq s s') -> (eql s s').
+  Proof.
+    Unfold eq Equal eql Lists.eq Lists.Raw.eq Lists.Raw.Equal.
+    Intros s s'.
+    Elim (to_slist s); Unfold Lists.In Lists.Raw.In; 
+      Simpl; Intros l Hl.
+    Elim (to_slist s'); Unfold Lists.In Lists.Raw.In; 
+      Simpl; Intros l' Hl'.
+    Ground.
+   Save.
+
+  Lemma eql_eq : (s,s':t)(eql s s') -> (eq s s').
+  Proof.
+    Unfold eq Equal eql Lists.eq Lists.Raw.eq Lists.Raw.Equal.
+    Intros s s'.
+    Elim (to_slist s); Unfold Lists.In Lists.Raw.In; 
+      Simpl; Intros l Hl.
+    Elim (to_slist s'); Unfold Lists.In Lists.Raw.In; 
+      Simpl; Intros l' Hl'.
+    Ground.
+  Save.
+
+  Lemma lt_not_eq : (s,s':t)(lt s s') -> ~(eq s s').
+  Proof.
+    Intros s s' H; Intro.
+    Generalize (eq_eql s s' H0).
+    Generalize H; Unfold lt eql.
+    Elim (to_slist s); Intros l Hl.
+    Elim (to_slist s'); Intros l' Hl'.
+    Exact (!Lists.lt_not_eq l l').
+  Save.
+  
+  Definition compare: (s,s':t)(Compare lt eq s s').
+  Proof.
+    Intros s s'.
+    Cut (lt s s') -> (Compare lt eq s s').    
+    Cut (eq s s') -> (Compare lt eq s s'). 
+    Cut (lt s' s) -> (Compare lt eq s s'). 
+    Unfold 1 4 lt.
+    Generalize (eql_eq s s'); Unfold eql.
+    Elim (to_slist s); Intros l Hl.
+    Elim (to_slist s'); Intros l' Hl'.
+    Elim (Lists.compare l l'); Intuition.
+    Constructor 3; Trivial.
+    Constructor 2; Trivial.
+    Constructor 1; Trivial.
+  Defined.
+
+End Make.
+
+
+
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 5dfc8ac8eb..122de1e2de 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -146,7 +146,7 @@ Apply lt_reg_r; Auto.
 Intuition; Elim H1; Simpl; Trivial.
 Qed.
 
-Lemma Z_rec : (P:Z->Type)(P `0`) -> 
+Lemma natlike_rec2 : (P:Z->Type)(P `0`) -> 
         ((z:Z)`0<z` -> (P (Zpred z)) -> (P z)) -> (z:Z)`0<=z` -> (P z).
 Proof.
 Intros P Ho Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf).