suppression de FSets (redevient une contrib)

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

1 files changed, 0 insertions, 706 deletions

diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
deleted file mode 100644
index 7efc27245..000000000
--- a/theories/FSets/FSetBridge.v
+++ /dev/null
@@ -1,706 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(** This module implements bridges (as functors) from dependent
-    to/from non-dependent set signature. *)
-
-Require Export FSetInterface.
-Set Implicit Arguments.
-Set Ground Depth 2.
-
-(** * 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)(s:t)(i:A) 
-   { r : A | (EX l:(list elt) | 
-                  (Unique E.eq l) /\
-                  ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
-                  r = (fold_right f i l)) }.
-  Proof.
-    Intros; Exists (!fold A f s i); Exact (fold_1 s i f).
-  Save.  
-
-  Definition cardinal :
-    (s:t) { r : nat | (EX l:(list elt) | 
-                              (Unique E.eq l) /\ 
-                              ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
-                              r = (length l)) }.
-  Proof.
-    Intros; Exists (cardinal s); Exact (cardinal_1 s).
-  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 := [s]let (f,_)= (M.cardinal s) in f.
-
-  Lemma cardinal_1 : 
-    (s:t)(EX l:(list elt) | 
-             (Unique E.eq l) /\
-             ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
-             (cardinal s)=(length l)).
-  Proof.
-    Intros; Unfold cardinal; Case (M.cardinal s); Ground.
-  Qed.
-
-  Definition fold : (B:Set)(elt->B->B)->t->B->B :=  
-       [B,f,i,s]let (fold,_)= (M.fold f i s) in fold.
-
-  Lemma fold_1: 
-   (s:t)(A:Set)(i:A)(f:elt->A->A)
-   (EX l:(list elt) | 
-       (Unique E.eq l) /\ 
-       ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
-       (fold f s i)=(fold_right f i l)).
-  Proof.
-    Intros; Unfold fold; Case (M.fold f s i); 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. 
-    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.
-    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.
-