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, 1241 deletions

diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
deleted file mode 100644
index 5b6065c26..000000000
--- a/theories/FSets/FSetList.v
+++ /dev/null
@@ -1,1241 +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 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)(Hs:(Sort s))(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; Exists s; Split; Intuition.
-  Apply ME.Sort_Unique; Auto.
-  Induction s; Simpl; Trivial.
-  Rewrite Hrecs; Trivial.
-  Inversion_clear Hs; Trivial.
-  Qed.
-
-  Lemma cardinal_1 : 
-    (s:t)(Hs:(Sort s))(EX l:(list elt) | (Unique E.eq l) /\ 
-                                   ((x:elt)(In x s)<->(InList E.eq x l)) /\ (cardinal s)=(length l)).
-  Proof.
-  Intros; Exists s; Split; Intuition.
-  Apply ME.Sort_Unique; Auto.  
-  Unfold cardinal; Induction s; Simpl; Trivial.
-  Rewrite Hrecs; Trivial.
-  Inversion_clear Hs; Trivial.
-  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 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 (sorted s)). 
- 
- Definition cardinal := [s:t](Raw.cardinal s).
- Definition cardinal_1 := [s:t](Raw.cardinal_1 (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.