Duplication du fichier FSetProperties pour les ensembles Weak.

Du coup, factorisation d'une partie dans SetoidList. Ajout de 
lemmes suggeres par Evelyne C. Un oubli dans FSetWeakInterface 
concernant elements. 



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

9 files changed, 1143 insertions, 236 deletions

diff --git a/.depend.coq b/.depend.coq
index 483ca08ad..a00983c4b 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -9,10 +9,11 @@ theories/FSets/FSetFacts.vo: theories/FSets/FSetFacts.v theories/FSets/FSetInter
 theories/FSets/FSetProperties.vo: theories/FSets/FSetProperties.v theories/FSets/FSetInterface.vo theories/FSets/FSetFacts.vo
 theories/FSets/FSetEqProperties.vo: theories/FSets/FSetEqProperties.v theories/FSets/FSetProperties.vo theories/Bool/Zerob.vo theories/Bool/Sumbool.vo contrib/omega/Omega.vo
 theories/FSets/FSets.vo: theories/FSets/FSets.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FSetInterface.vo theories/FSets/FSetBridge.vo theories/FSets/FSetProperties.vo theories/FSets/FSetEqProperties.vo theories/FSets/FSetList.vo theories/FSets/FSetToFiniteSet.vo
+theories/FSets/FSetWeakProperties.vo: theories/FSets/FSetWeakProperties.v theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakFacts.vo
 theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories/Bool/Bool.vo theories/FSets/DecidableType.vo
 theories/FSets/FSetWeakList.vo: theories/FSets/FSetWeakList.v theories/FSets/FSetWeakInterface.vo
 theories/FSets/FSetWeakFacts.vo: theories/FSets/FSetWeakFacts.v theories/FSets/FSetWeakInterface.vo
-theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/FSets/DecidableType.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetWeakList.vo
+theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/FSets/DecidableType.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetProperties.vo theories/FSets/FSetWeakList.vo
 theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/FSets/FSetInterface.vo
 theories/FSets/FMapList.vo: theories/FSets/FMapList.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo
 theories/FSets/FMaps.vo: theories/FSets/FMaps.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FMapPositive.vo theories/FSets/FMapIntMap.vo
@@ -217,10 +218,11 @@ theories/FSets/FSetFacts.vo: theories/FSets/FSetFacts.v theories/FSets/FSetInter
 theories/FSets/FSetProperties.vo: theories/FSets/FSetProperties.v theories/FSets/FSetInterface.vo theories/FSets/FSetFacts.vo
 theories/FSets/FSetEqProperties.vo: theories/FSets/FSetEqProperties.v theories/FSets/FSetProperties.vo theories/Bool/Zerob.vo theories/Bool/Sumbool.vo contrib/omega/Omega.vo
 theories/FSets/FSets.vo: theories/FSets/FSets.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FSetInterface.vo theories/FSets/FSetBridge.vo theories/FSets/FSetProperties.vo theories/FSets/FSetEqProperties.vo theories/FSets/FSetList.vo theories/FSets/FSetToFiniteSet.vo
+theories/FSets/FSetWeakProperties.vo: theories/FSets/FSetWeakProperties.v theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakFacts.vo
 theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories/Bool/Bool.vo theories/FSets/DecidableType.vo
 theories/FSets/FSetWeakList.vo: theories/FSets/FSetWeakList.v theories/FSets/FSetWeakInterface.vo
 theories/FSets/FSetWeakFacts.vo: theories/FSets/FSetWeakFacts.v theories/FSets/FSetWeakInterface.vo
-theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/FSets/DecidableType.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetWeakList.vo
+theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/FSets/DecidableType.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetProperties.vo theories/FSets/FSetWeakList.vo
 theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/FSets/FSetInterface.vo
 theories/FSets/FMapList.vo: theories/FSets/FMapList.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo
 theories/FSets/FMaps.vo: theories/FSets/FMaps.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FMapPositive.vo theories/FSets/FMapIntMap.vo
@@ -266,54 +268,6 @@ theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.
 theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
 theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
-theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
-theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
-theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
-theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
-theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo
-theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo
-theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplete.vo theories/Arith/Max.vo
-theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
-theories/Reals/Binomial.vo: theories/Reals/Binomial.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo
-theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
-theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binomial.vo
-theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
-theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
-theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Arith/Max.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo
-theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo
-theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo
-theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo
-theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
-theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo
-theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo
-theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo
-theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
-theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
-theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
-theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
-theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
-theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo
-theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo
-theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
-theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo
-theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo
-theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo
-theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo
-theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo
-theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo
-theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo
 theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v theories/Relations/Relation_Definitions.vo
 theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
 theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo
diff --git a/Makefile b/Makefile
index 45ae6c8c9..9c2a02e61 100644
--- a/Makefile
+++ b/Makefile
@@ -871,7 +871,7 @@ FSETSBASEVO=\
  theories/FSets/FSetInterface.vo     theories/FSets/FSetList.vo \
  theories/FSets/FSetBridge.vo        theories/FSets/FSetFacts.vo \
  theories/FSets/FSetProperties.vo    theories/FSets/FSetEqProperties.vo \
- theories/FSets/FSets.vo \
+ theories/FSets/FSets.vo             theories/FSets/FSetWeakProperties.vo \
  theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakList.vo \
  theories/FSets/FSetWeakFacts.vo     theories/FSets/FSetWeak.vo \
  theories/FSets/FMapInterface.vo     theories/FSets/FMapList.vo \
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index b27e08240..a0414cd34 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -704,6 +704,11 @@ assert (f a || g a = true <-> f a = true \/ g a = true).
 tauto.
 Qed.
 
+Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').
+Proof.
+unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.
+Qed.
+
 (** Properties of [for_all] *)
 
 Lemma for_all_mem_1: forall s, 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 4d8a78a14..44abc0f1b 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -21,49 +21,13 @@ Require Import FSetFacts.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-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) :=
-  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). 
-
-(** Compatibility of a two-argument function with respect to two equalities. *)
-Definition compat_op (f : A -> B -> B) :=
-  forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
-
-(** Compatibility of a function upon natural numbers. *)
-Definition compat_nat (f : A -> nat) :=
-  forall x x' : A, eqA x x' -> f x = f x'.
-
-End Misc.
-Hint Unfold transpose compat_op compat_nat.
-
+Hint Unfold transpose compat_op.
 Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence.
 
-Ltac trans_st x := match goal with 
-  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
-     apply (Seq_trans _ _ H) with x; auto
- end.
-
-Ltac sym_st := match goal with 
-  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
-     apply (Seq_sym _ _ H); auto
- end.
-
-Ltac refl_st := match goal with 
-  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
-     apply (Seq_refl _ _ H); auto
- end.
-
-Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A).
-Proof. auto. Qed.
-
 Module Properties (M: S).
-  Module ME := OrderedTypeFacts M.E.  
-  Import ME.
+  Module ME:=OrderedTypeFacts(M.E).
+  Import ME. (* for ME.eq_dec *)
+  Import M.E.
   Import M.
   Import Logic. (* to unmask [eq] *)  
   Import Peano. (* to unmask [lt] *)
@@ -82,26 +46,29 @@ Module Properties (M: S).
   Qed.
 
   Section BasicProperties.
-  Variable s s' s'' s1 s2 s3 : t.
-  Variable x : elt.
 
   (** properties of [Equal] *)
 
-  Lemma equal_refl : s[=]s.
+  Lemma equal_refl : forall s, s[=]s.
   Proof.
-  apply eq_refl.
+  unfold Equal; intuition.
   Qed.
 
-  Lemma equal_sym : s[=]s' -> s'[=]s.
+  Lemma equal_sym : forall s s', s[=]s' -> s'[=]s.
   Proof.
-  apply eq_sym. 
+  unfold Equal; intros.
+  rewrite H; intuition.
   Qed.
 
-  Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3.
+  Lemma equal_trans : forall s1 s2 s3, s1[=]s2 -> s2[=]s3 -> s1[=]s3.
   Proof.
-  intros; apply eq_trans with s2; auto.
+  unfold Equal; intros.
+  rewrite H; exact (H0 a).
   Qed.
 
+  Variable s s' s'' s1 s2 s3 : t.
+  Variable x x' : elt.
+
   (** properties of [Subset] *)
   
   Lemma subset_refl : s[<=]s. 
@@ -179,6 +146,11 @@ Module Properties (M: S).
   unfold Equal; intros; set_iff; intuition.
   rewrite <- H1; auto.
   Qed.
+ 
+  Lemma add_add : add x (add x' s) [=] add x' (add x s).
+  Proof. 
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
 
   (** properties of [remove] *)
 
@@ -190,7 +162,7 @@ Module Properties (M: S).
 
   Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.
   Proof.
-  intros; rewrite H; apply eq_refl.
+  intros; rewrite H; apply equal_refl.
   Qed.
 
   (** properties of [add] and [remove] *)
@@ -228,12 +200,12 @@ Module Properties (M: S).
 
   Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.
   Proof.
-  intros; rewrite H; apply eq_refl.
+  intros; rewrite H; apply equal_refl.
   Qed.
 
   Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.
   Proof.
-  intros; rewrite H; apply eq_refl.
+  intros; rewrite H; apply equal_refl.
   Qed.
 
   Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
@@ -266,6 +238,16 @@ Module Properties (M: S).
   unfold Subset; intros H H0 a; set_iff; intuition.
   Qed.
 
+  Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.
+  Proof. 
+  unfold Subset; intros H a; set_iff; intuition.
+  Qed.
+
+  Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.
+  Proof. 
+  unfold Subset; intros H a; set_iff; intuition.
+  Qed.
+
   Lemma empty_union_1 : Empty s -> union s s' [=] s'.
   Proof.
   unfold Equal, Empty; intros; set_iff; firstorder.
@@ -295,12 +277,12 @@ Module Properties (M: S).
 
   Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.
   Proof.
-  intros; rewrite H; apply eq_refl.
+  intros; rewrite H; apply equal_refl.
   Qed.
 
   Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.
   Proof.
-  intros; rewrite H; apply eq_refl.
+  intros; rewrite H; apply equal_refl.
   Qed.
 
   Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
@@ -452,140 +434,14 @@ Module Properties (M: S).
     empty_diff_2 union_Add inter_Add union_Equal inter_Add_2 not_in_union 
     inter_subset_1 inter_subset_2 inter_subset_3 diff_subset diff_subset_equal 
     remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
-    Equal_remove : set.
-
-  Notation NoDup := (NoDupA E.eq).
-  Notation EqList := (eqlistA E.eq).
-
-  Section NoDupA_Remove.
-
-  Let ListAdd x l l' := forall y : elt, ME.In y l' <-> E.eq x y \/ ME.In y l.
-
-  Lemma removeA_add :
-    forall s s' x x', NoDup s -> NoDup (x' :: s') ->
-    ~ E.eq x x' -> ~ ME.In x s -> 
-    ListAdd x s (x' :: s') -> ListAdd x (removeA eq_dec x' s) s'.
-  Proof.
-   unfold ListAdd; intros.
-   inversion_clear H0.
-   rewrite removeA_InA; auto; [apply E.eq_trans|].
-   split; intros.
-   destruct (eq_dec x y); auto; intros.
-   right; split; auto.
-   destruct (H3 y); clear H3.
-   destruct H6; intuition.
-   swap H4; apply In_eq with y; auto.
-   destruct H0.
-   assert (ME.In y (x' :: s')) by rewrite H3; auto.
-   inversion_clear H6; auto.
-   elim H1; apply E.eq_trans with y; auto.
-   destruct H0.
-   assert (ME.In y (x' :: s')) by rewrite H3; auto.
-   inversion_clear H7; auto.
-   elim H6; auto.
-  Qed.
-
-  Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
-  Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
-  Variables (i:A).
-
-  Lemma removeA_fold_right_0 :
-    forall s x, NoDup s -> ~ME.In x s ->
-    eqA (fold_right f i s) (fold_right f i (removeA eq_dec x s)).
-  Proof.
-   simple induction s; simpl; intros.
-   refl_st.
-   inversion_clear H0.
-   destruct (eq_dec x a); simpl; intros.
-   absurd_hyp e; auto.
-   apply Comp; auto. 
-  Qed.   
-
-  Lemma removeA_fold_right :
-    forall s x, NoDup s -> ME.In x s ->
-    eqA (fold_right f i s) (f x (fold_right f i (removeA eq_dec x s))).
-  Proof.
-   simple induction s; simpl.  
-   inversion_clear 2.
-   intros.
-   inversion_clear H0.
-   destruct (eq_dec x a); simpl; intros.
-   apply Comp; auto. 
-   apply removeA_fold_right_0; auto.
-   swap H2; apply ME.In_eq with x; auto.
-   inversion_clear H1. 
-   destruct n; auto.
-   trans_st (f a (f x (fold_right f i (removeA eq_dec x l)))).
-  Qed.   
-
-  Lemma fold_right_equal :
-    forall s s', NoDup s -> NoDup s' ->
-    EqList s s' -> eqA (fold_right f i s) (fold_right f i s').
-  Proof.
-   simple induction s.
-   destruct s'; simpl.
-   intros; refl_st; auto.
-   unfold eqlistA; intros.
-   destruct (H1 t0).
-   assert (X : ME.In t0 nil); auto; inversion X.
-   intros x l Hrec s' N N' E; simpl in *.
-   trans_st (f x (fold_right f i (removeA eq_dec x s'))).
-   apply Comp; auto.
-   apply Hrec; auto.
-   inversion N; auto.
-   apply removeA_NoDupA; auto; apply E.eq_trans.
-   apply removeA_eqlistA; auto; [apply E.eq_trans|].
-   inversion_clear N; auto.
-   sym_st.
-   apply removeA_fold_right; auto.
-   unfold eqlistA in E.
-   rewrite <- E; auto.
-  Qed.
-
-  Lemma fold_right_add :
-    forall s' s x, NoDup s -> NoDup s' -> ~ ME.In x s ->
-    ListAdd x s s' -> eqA (fold_right f i s') (f x (fold_right f i s)).
-  Proof.   
-   simple induction s'.
-   unfold ListAdd; intros.
-   destruct (H2 x); clear H2.
-   assert (X : ME.In x nil); auto; inversion X.
-   intros x' l' Hrec s x N N' IN EQ; simpl.
-   (* if x=x' *)
-   destruct (eq_dec x x').
-   apply Comp; auto.
-   apply fold_right_equal; auto.
-   inversion_clear N'; trivial.
-   unfold eqlistA; unfold ListAdd in EQ; intros.
-   destruct (EQ x0); clear EQ.
-   split; intros.
-   destruct H; auto.
-   inversion_clear N'.
-   destruct H2; apply In_eq with x0; auto; order.
-   assert (X:ME.In x0 (x' :: l')); auto; inversion_clear X; auto.
-   destruct IN; apply In_eq with x0; auto; order.
-   (* else x<>x' *)   
-   trans_st (f x' (f x (fold_right f i (removeA eq_dec x' s)))).
-   apply Comp; auto.
-   apply Hrec; auto.
-   apply removeA_NoDupA; auto; apply E.eq_trans.
-   inversion_clear N'; auto.
-   rewrite removeA_InA; auto; [apply E.eq_trans|intuition].
-   apply removeA_add; auto.
-   trans_st (f x (f x' (fold_right f i (removeA eq_dec x' s)))).
-   apply Comp; auto.
-   sym_st.
-   apply removeA_fold_right; auto.
-   destruct (EQ x'). 
-   destruct H; auto; destruct n; auto.
-  Qed.
-
-  End NoDupA_Remove.
+    Equal_remove add_add : set.
 
   (** * Alternative (weaker) specifications for [fold] *)
 
   Section Old_Spec_Now_Properties. 
 
+  Notation NoDup := (NoDupA E.eq).
+
   (** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
         takes the set elements was unspecified. This specification reflects this fact: 
   *)
@@ -634,7 +490,9 @@ Module Properties (M: S).
   intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); 
     destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
   rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
-  apply fold_right_add with (eqA := eqA); auto.
+  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
+  eauto.
+  exact eq_dec.
   rewrite <- Hl1; auto.
   intros; rewrite <- Hl1; rewrite <- Hl'1; auto.
   Qed.
@@ -961,7 +819,23 @@ Module Properties (M: S).
   rewrite (inter_subset_equal H); auto with arith.
   Qed.
 
-  Lemma union_inter_cardinal :
+  Lemma subset_cardinal_lt : 
+   forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.
+  Proof. 
+  intros.
+  rewrite <- (diff_inter_cardinal s' s).
+  rewrite (inter_sym s' s).
+  rewrite (inter_subset_equal H).
+  generalize (@cardinal_inv_1 (diff s' s)).
+  destruct (cardinal (diff s' s)).
+  intro H2; destruct (H2 (refl_equal _) x).
+  set_iff; auto.
+  intros _.
+  change (0 + cardinal s < S n + cardinal s).
+  apply Plus.plus_lt_le_compat; auto with arith.
+  Qed. 
+
+  Theorem union_inter_cardinal :
    forall s s', cardinal (union s s') + cardinal (inter s s')  = cardinal s  + cardinal s' .
   Proof.
   intros.
@@ -970,6 +844,15 @@ Module Properties (M: S).
   apply fold_union_inter with (eqA:=@eq nat); auto.
   Qed.
 
+  Lemma union_cardinal_inter : 
+   forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
+  Proof.
+  intros.
+  rewrite <- union_inter_cardinal.
+  rewrite Plus.plus_comm.
+  auto with arith.
+  Qed.
+
   Lemma union_cardinal_le : 
    forall s s', cardinal (union s s') <= cardinal s  + cardinal s'.
   Proof.
diff --git a/theories/FSets/FSetWeak.v b/theories/FSets/FSetWeak.v
index e6b35f84c..ccf590ca3 100644
--- a/theories/FSets/FSetWeak.v
+++ b/theories/FSets/FSetWeak.v
@@ -11,4 +11,5 @@
 Require Export DecidableType.
 Require Export FSetWeakInterface.
 Require Export FSetFacts.
+Require Export FSetProperties.
 Require Export FSetWeakList.
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
index 598a75924..27e4a5ccf 100644
--- a/theories/FSets/FSetWeakInterface.v
+++ b/theories/FSets/FSetWeakInterface.v
@@ -229,6 +229,7 @@ Module Type S.
   (** Specification of [elements] *)
   Parameter elements_1 : In x s -> InA E.eq x (elements s).
   Parameter elements_2 : InA E.eq x (elements s) -> In x s.
+  Parameter elements_3 : NoDupA E.eq (elements s).
 
   (** Specification of [choose] *)
   Parameter choose_1 : choose s = Some x -> In x s.
@@ -243,6 +244,7 @@ Module Type S.
     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 filter_1 filter_2 filter_3 for_all_1
-    for_all_2 exists_1 exists_2 partition_1 partition_2 elements_1 elements_2.
+    for_all_2 exists_1 exists_2 partition_1 partition_2 elements_1 elements_2
+    elements_3.
 
 End S.
diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v
new file mode 100644
index 000000000..44977da2a
--- /dev/null
+++ b/theories/FSets/FSetWeakProperties.v
@@ -0,0 +1,896 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(** * Finite sets library *)
+
+(** NB: this file is a clone of [FSetProperties] for weak sets
+     and should remain so until we find a way to share the two. *)
+
+(** This functor derives additional properties from [FSetWeakInterface.S].
+    Contrary to the functor in [FSetWeakEqProperties] it uses 
+    predicates over sets instead of sets operations, i.e.
+    [In x s] instead of [mem x s=true], 
+    [Equal s s'] instead of [equal s s'=true], etc. *)
+
+Require Export FSetWeakInterface. 
+Require Import FSetWeakFacts.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Hint Unfold transpose compat_op.
+Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence.
+
+Module Properties (M: S).
+  Import M.E.
+  Import M.
+  Import Logic. (* to unmask [eq] *)  
+  Import Peano. (* to unmask [lt] *)
+  
+   (** Results about lists without duplicates *)
+
+  Module FM := Facts M.
+  Import FM.
+
+  Definition Add (x : elt) (s s' : t) :=
+    forall y : elt, In y s' <-> E.eq x y \/ In y s.
+
+  Lemma In_dec : forall x s, {In x s} + {~ In x s}.
+  Proof.
+  intros; generalize (mem_iff s x); case (mem x s); intuition.
+  Qed.
+
+  Section BasicProperties.
+
+  (** properties of [Equal] *)
+
+  Lemma equal_refl : forall s, s[=]s.
+  Proof.
+  unfold Equal; intuition.
+  Qed.
+
+  Lemma equal_sym : forall s s', s[=]s' -> s'[=]s.
+  Proof.
+  unfold Equal; intros.
+  rewrite H; intuition.
+  Qed.
+
+  Lemma equal_trans : forall s1 s2 s3, s1[=]s2 -> s2[=]s3 -> s1[=]s3.
+  Proof.
+  unfold Equal; intros.
+  rewrite H; exact (H0 a).
+  Qed.
+
+  Variable s s' s'' s1 s2 s3 : t.
+  Variable x x' : elt.
+
+  (** properties of [Subset] *)
+  
+  Lemma subset_refl : s[<=]s. 
+  Proof.
+  unfold Subset; intuition.
+  Qed.
+
+  Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
+  Proof.
+  unfold Subset, Equal; intuition.
+  Qed.
+
+  Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
+  Proof.
+  unfold Subset; intuition.
+  Qed.
+
+  Lemma subset_equal : s[=]s' -> s[<=]s'.
+  Proof.
+  unfold Subset, Equal; firstorder.
+  Qed.
+
+  Lemma subset_empty : empty[<=]s.
+  Proof.
+  unfold Subset; intros a; set_iff; intuition.
+  Qed.
+
+  Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2.
+  Proof.
+  unfold Subset; intros H a; set_iff; intuition.
+  Qed.
+
+  Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3.
+  Proof.
+  unfold Subset; intros H a; set_iff; intuition.
+  Qed.
+
+  Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2.
+  Proof.
+  unfold Subset; intros H H0 a; set_iff; intuition.
+  rewrite <- H2; auto.
+  Qed.
+
+  Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2.
+  Proof.
+  unfold Subset; intuition.
+  Qed.
+
+  Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.
+  Proof.
+  unfold Subset; intuition.
+  Qed.
+ 
+  Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
+  Proof.
+  unfold Subset, Equal; split; intros; intuition; generalize (H a); intuition.
+  Qed.
+
+  (** properties of [empty] *)
+
+  Lemma empty_is_empty_1 : Empty s -> s[=]empty.
+  Proof.
+  unfold Empty, Equal; intros; generalize (H a); set_iff; tauto.
+  Qed.
+
+  Lemma empty_is_empty_2 : s[=]empty -> Empty s.
+  Proof.
+  unfold Empty, Equal; intros; generalize (H a); set_iff; tauto.
+  Qed.
+
+  (** properties of [add] *)
+
+  Lemma add_equal : In x s -> add x s [=] s.
+  Proof.
+  unfold Equal; intros; set_iff; intuition.
+  rewrite <- H1; auto.
+  Qed.
+ 
+  Lemma add_add : add x (add x' s) [=] add x' (add x s).
+  Proof. 
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
+
+  (** properties of [remove] *)
+
+  Lemma remove_equal : ~ In x s -> remove x s [=] s.
+  Proof.
+  unfold Equal; intros; set_iff; intuition.
+  rewrite H1 in H; auto.
+  Qed.
+
+  Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.
+  Proof.
+  intros; rewrite H; apply equal_refl.
+  Qed.
+
+  (** properties of [add] and [remove] *)
+
+  Lemma add_remove : In x s -> add x (remove x s) [=] s.
+  Proof.
+  unfold Equal; intros; set_iff; elim (eq_dec x a); intuition.
+  rewrite <- H1; auto.
+  Qed.
+
+  Lemma remove_add : ~In x s -> remove x (add x s) [=] s.
+  Proof.
+  unfold Equal; intros; set_iff; elim (eq_dec x a); intuition.
+  rewrite H1 in H; auto.
+  Qed.
+
+  (** properties of [singleton] *)
+
+  Lemma singleton_equal_add : singleton x [=] add x empty.
+  Proof.
+  unfold Equal; intros; set_iff; intuition.
+  Qed.
+
+  (** properties of [union] *)
+
+  Lemma union_sym : union s s' [=] union s' s.
+  Proof.
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
+
+  Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'.
+  Proof.
+  unfold Subset, Equal; intros; set_iff; intuition.
+  Qed.
+
+  Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.
+  Proof.
+  intros; rewrite H; apply equal_refl.
+  Qed.
+
+  Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.
+  Proof.
+  intros; rewrite H; apply equal_refl.
+  Qed.
+
+  Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
+  Proof.
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
+
+  Lemma add_union_singleton : add x s [=] union (singleton x) s.
+  Proof.
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
+
+  Lemma union_add : union (add x s) s' [=] add x (union s s').
+  Proof.
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
+
+  Lemma union_subset_1 : s [<=] union s s'.
+  Proof.
+  unfold Subset; intuition.
+  Qed.
+
+  Lemma union_subset_2 : s' [<=] union s s'.
+  Proof.
+  unfold Subset; intuition.
+  Qed.
+
+  Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''.
+  Proof.
+  unfold Subset; intros H H0 a; set_iff; intuition.
+  Qed.
+
+  Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.
+  Proof. 
+  unfold Subset; intros H a; set_iff; intuition.
+  Qed.
+
+  Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.
+  Proof. 
+  unfold Subset; intros H a; set_iff; intuition.
+  Qed.
+
+  Lemma empty_union_1 : Empty s -> union s s' [=] s'.
+  Proof.
+  unfold Equal, Empty; intros; set_iff; firstorder.
+  Qed.
+
+  Lemma empty_union_2 : Empty s -> union s' s [=] s'.
+  Proof.
+  unfold Equal, Empty; intros; set_iff; firstorder.
+  Qed.
+
+  Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s'). 
+  Proof.
+  intros; set_iff; intuition. 
+  Qed.  
+
+  (** properties of [inter] *)
+
+  Lemma inter_sym : inter s s' [=] inter s' s.
+  Proof.
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
+
+  Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s.
+  Proof.
+  unfold Equal; intros; set_iff; intuition.
+  Qed.
+
+  Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.
+  Proof.
+  intros; rewrite H; apply equal_refl.
+  Qed.
+
+  Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.
+  Proof.
+  intros; rewrite H; apply equal_refl.
+  Qed.
+
+  Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
+  Proof.
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
+
+  Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s'').
+  Proof.
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
+
+  Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s'').
+  Proof.
+  unfold Equal; intros; set_iff; tauto.
+  Qed.
+
+  Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s').
+  Proof.
+  unfold Equal; intros; set_iff; intuition.
+  rewrite <- H1; auto.
+  Qed.
+
+  Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'.
+  Proof.
+  unfold Equal; intros; set_iff; intuition.
+  destruct H; rewrite H0; auto.
+  Qed.
+
+  Lemma empty_inter_1 : Empty s -> Empty (inter s s').
+  Proof.
+  unfold Empty; intros; set_iff; firstorder.
+  Qed.
+
+  Lemma empty_inter_2 : Empty s' -> Empty (inter s s').
+  Proof.
+  unfold Empty; intros; set_iff; firstorder.
+  Qed.
+
+  Lemma inter_subset_1 : inter s s' [<=] s.
+  Proof.
+  unfold Subset; intro a; set_iff; tauto.
+  Qed.
+
+  Lemma inter_subset_2 : inter s s' [<=] s'.
+  Proof.
+  unfold Subset; intro a; set_iff; tauto.
+  Qed.
+
+  Lemma inter_subset_3 :
+   s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'.
+  Proof.
+  unfold Subset; intros H H' a; set_iff; intuition.
+  Qed.
+
+  (** properties of [diff] *)
+
+  Lemma empty_diff_1 : Empty s -> Empty (diff s s'). 
+  Proof.
+  unfold Empty, Equal; intros; set_iff; firstorder.
+  Qed.
+
+  Lemma empty_diff_2 : Empty s -> diff s' s [=] s'.
+  Proof.
+  unfold Empty, Equal; intros; set_iff; firstorder.
+  Qed.
+
+  Lemma diff_subset : diff s s' [<=] s.
+  Proof.
+  unfold Subset; intros a; set_iff; tauto.
+  Qed.
+
+  Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty.
+  Proof.
+  unfold Subset, Equal; intros; set_iff; intuition; absurd (In a empty); auto.
+  Qed.
+
+  Lemma remove_diff_singleton :
+   remove x s [=] diff s (singleton x).
+  Proof.
+  unfold Equal; intros; set_iff; intuition.
+  Qed.
+
+  Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty. 
+  Proof.
+  unfold Equal; intros; set_iff; intuition; absurd (In a empty); auto.
+  Qed.
+
+  Lemma diff_inter_all : union (diff s s') (inter s s') [=] s.
+  Proof.
+  unfold Equal; intros; set_iff; intuition.
+  elim (In_dec a s'); auto.
+  Qed.
+
+  (** properties of [Add] *)
+
+  Lemma Add_add : Add x s (add x s).
+  Proof.
+   unfold Add; intros; set_iff; intuition.
+  Qed.
+
+  Lemma Add_remove : In x s -> Add x (remove x s) s. 
+  Proof. 
+    unfold Add; intros; set_iff; intuition.
+    elim (eq_dec x y); auto.
+    rewrite <- H1; auto.
+  Qed.
+
+  Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s'').
+  Proof. 
+  unfold Add; intros; set_iff; rewrite H; tauto.
+  Qed.
+
+  Lemma inter_Add :
+   In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'').
+  Proof. 
+  unfold Add; intros; set_iff; rewrite H0; intuition.
+  rewrite <- H2; auto.
+  Qed.  
+
+  Lemma union_Equal :
+   In x s'' -> Add x s s' -> union s s'' [=] union s' s''.
+  Proof. 
+  unfold Add, Equal; intros; set_iff; rewrite H0; intuition. 
+  rewrite <- H1; auto.
+  Qed.  
+
+  Lemma inter_Add_2 :
+   ~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''.
+  Proof.
+  unfold Add, Equal; intros; set_iff; rewrite H0; intuition.
+  destruct H; rewrite H1; auto.
+  Qed.
+
+  End BasicProperties.
+
+  Hint Immediate equal_sym: set.
+  Hint Resolve equal_refl equal_trans : set.
+
+  Hint Immediate add_remove remove_add union_sym inter_sym: set.
+  Hint Resolve subset_refl subset_equal subset_antisym 
+    subset_trans subset_empty subset_remove_3 subset_diff subset_add_3 
+    subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
+    remove_equal singleton_equal_add union_subset_equal union_equal_1 
+    union_equal_2 union_assoc add_union_singleton union_add union_subset_1 
+    union_subset_2 union_subset_3 inter_subset_equal inter_equal_1 inter_equal_2
+    inter_assoc union_inter_1 union_inter_2 inter_add_1 inter_add_2
+    empty_inter_1 empty_inter_2 empty_union_1 empty_union_2 empty_diff_1 
+    empty_diff_2 union_Add inter_Add union_Equal inter_Add_2 not_in_union 
+    inter_subset_1 inter_subset_2 inter_subset_3 diff_subset diff_subset_equal 
+    remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
+    Equal_remove add_add : set.
+
+  (** * Alternative (weaker) specifications for [fold] *)
+
+  Section Old_Spec_Now_Properties. 
+
+  Notation NoDup := (NoDupA E.eq).
+
+  (** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
+        takes the set elements was unspecified. This specification reflects this fact: 
+  *)
+
+  Lemma fold_0 : 
+      forall s (A : Set) (i : A) (f : elt -> A -> A),
+      exists l : list elt,
+        NoDup l /\
+        (forall x : elt, In x s <-> InA E.eq x l) /\
+        fold f s i = fold_right f i l.
+  Proof.
+  intros; exists (rev (elements s)); split.
+  apply NoDupA_rev; auto.
+  exact E.eq_trans.
+  split; intros.
+  rewrite elements_iff; do 2 rewrite InA_alt.
+  split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
+  rewrite fold_left_rev_right.
+  apply fold_1.
+  Qed.
+
+  (** An alternate (and previous) specification for [fold] was based on 
+      the recursive structure of a set. It is now lemmas [fold_1] and 
+      [fold_2]. *)
+
+  Lemma fold_1 :
+   forall s (A : Set) (eqA : A -> A -> Prop) 
+     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+   Empty s -> eqA (fold f s i) i.
+  Proof.
+  unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))).
+  rewrite H3; clear H3.
+  generalize H H2; clear H H2; case l; simpl; intros.
+  refl_st.
+  elim (H e).
+  elim (H2 e); intuition. 
+  Qed.
+
+  Lemma fold_2 :
+   forall s s' x (A : Set) (eqA : A -> A -> Prop)
+     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+   compat_op E.eq eqA f ->
+   transpose eqA f ->
+   ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
+  Proof.
+  intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); 
+    destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
+  rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
+  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
+  eauto.
+  exact eq_dec.
+  rewrite <- Hl1; auto.
+  intros; rewrite <- Hl1; rewrite <- Hl'1; auto.
+  Qed.
+
+  (** Similar specifications for [cardinal]. *)
+
+  Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
+  Proof.
+  intros; rewrite cardinal_1; rewrite M.fold_1.
+  symmetry; apply fold_left_length; auto.
+  Qed.
+
+  Lemma cardinal_0 :
+     forall s, exists l : list elt,
+        NoDupA E.eq l /\
+        (forall x : elt, In x s <-> InA E.eq x l) /\ 
+        cardinal s = length l.
+  Proof. 
+  intros; exists (elements s); intuition; apply cardinal_1.
+  Qed.
+
+  Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
+  Proof.
+  intros; rewrite cardinal_fold; apply fold_1; auto.
+  Qed.
+
+  Lemma cardinal_2 :
+    forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s).
+  Proof.
+  intros; do 2 rewrite cardinal_fold.
+  change S with ((fun _ => S) x).
+  apply fold_2; auto.
+  Qed.
+
+  End Old_Spec_Now_Properties.
+
+  (** * Induction principle over sets *)
+
+  Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s. 
+  Proof. 
+    intros s; rewrite M.cardinal_1; intros H a; red.
+    rewrite elements_iff.
+    destruct (elements s); simpl in *; discriminate || inversion 1.
+  Qed.
+  Hint Resolve cardinal_inv_1.
+ 
+  Lemma cardinal_inv_2 :
+   forall s n, cardinal s = S n -> { x : elt | In x s }.
+  Proof. 
+    intros; rewrite M.cardinal_1 in H.
+    generalize (elements_2 (s:=s)).
+    destruct (elements s); try discriminate. 
+    exists e; auto.
+  Qed.
+
+  Lemma Equal_cardinal_aux :
+   forall n s s', cardinal s = n -> s[=]s' -> cardinal s = cardinal s'.
+  Proof.
+     simple induction n; intros.
+     rewrite H; symmetry .
+     apply cardinal_1.
+     rewrite <- H0; auto.
+     destruct (cardinal_inv_2 H0) as (x,H2).
+     revert H0.
+     rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.
+     rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); auto with set.
+     rewrite H1 in H2; auto with set.
+  Qed.
+
+  Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
+  Proof. 
+    intros; apply Equal_cardinal_aux with (cardinal s); auto.
+  Qed.
+
+  Add Morphism cardinal : cardinal_m.
+  Proof.
+  exact Equal_cardinal.
+  Qed.
+
+  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
+
+  Lemma cardinal_induction :
+   forall P : t -> Type,
+   (forall s, Empty s -> P s) ->
+   (forall s s', P s -> forall x, ~In x s -> Add x s s' -> P s') ->
+   forall n s, cardinal s = n -> P s.
+  Proof.
+  simple induction n; intros; auto.
+  destruct (cardinal_inv_2 H) as (x,H0). 
+  apply X0 with (remove x s) x; auto.
+  apply X1; auto.
+  rewrite (cardinal_2 (x:=x)(s:=remove x s)(s':=s)) in H; auto.
+  Qed.
+
+  Lemma set_induction :
+   forall P : t -> Type,
+   (forall s : t, Empty s -> P s) ->
+   (forall s s' : t, P s -> forall x : elt, ~In x s -> Add x s s' -> P s') ->
+   forall s : t, P s.
+  Proof.
+  intros; apply cardinal_induction with (cardinal s); auto.
+  Qed.  
+
+  (** Other properties of [fold]. *)
+
+  Section Fold. 
+  Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
+  Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
+
+  Section Fold_1. 
+  Variable i i':A.
+
+  Lemma fold_empty : eqA (fold f empty i) i.
+  Proof. 
+  apply fold_1; auto.
+  Qed.
+
+  Lemma fold_equal : 
+   forall s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
+  Proof. 
+  intros s; pattern s; apply set_induction; clear s; intros.
+  trans_st i.
+  apply fold_1; auto.
+  sym_st; apply fold_1; auto.
+  rewrite <- H0; auto.
+  trans_st (f x (fold f s i)).
+  apply fold_2 with (eqA := eqA); auto.
+  sym_st; apply fold_2 with (eqA := eqA); auto.
+  unfold Add in *; intros.
+  rewrite <- H2; auto.
+  Qed.
+   
+  Lemma fold_add : forall s x, ~In x s -> 
+   eqA (fold f (add x s) i) (f x (fold f s i)).
+  Proof. 
+  intros; apply fold_2 with (eqA := eqA); auto.
+  Qed.
+
+  Lemma add_fold : forall s x, In x s -> 
+   eqA (fold f (add x s) i) (fold f s i).
+  Proof.
+  intros; apply fold_equal; auto with set.
+  Qed.
+
+  Lemma remove_fold_1: forall s x, In x s -> 
+   eqA (f x (fold f (remove x s) i)) (fold f s i).
+  Proof.
+  intros.
+  sym_st.
+  apply fold_2 with (eqA:=eqA); auto.
+  Qed.
+
+  Lemma remove_fold_2: forall s x, ~In x s -> 
+   eqA (fold f (remove x s) i) (fold f s i).
+  Proof.
+  intros.
+  apply fold_equal; auto with set.
+  Qed.
+
+  Lemma fold_commutes : forall s x, 
+   eqA (fold f s (f x i)) (f x (fold f s i)).
+  Proof.
+  intros; pattern s; apply set_induction; clear s; intros.
+  trans_st (f x i).
+  apply fold_1; auto.
+  sym_st.
+  apply Comp; auto.
+  apply fold_1; auto.
+  trans_st (f x0 (fold f s (f x i))).
+  apply fold_2 with (eqA:=eqA); auto.
+  trans_st (f x0 (f x (fold f s i))).
+  trans_st (f x (f x0 (fold f s i))).
+  apply Comp; auto.
+  sym_st.
+  apply fold_2 with (eqA:=eqA); auto.
+  Qed.
+
+  Lemma fold_init : forall s, eqA i i' -> 
+   eqA (fold f s i) (fold f s i').
+  Proof. 
+  intros; pattern s; apply set_induction; clear s; intros.
+  trans_st i.
+  apply fold_1; auto.
+  trans_st i'.
+  sym_st; apply fold_1; auto.
+  trans_st (f x (fold f s i)).
+  apply fold_2 with (eqA:=eqA); auto.
+  trans_st (f x (fold f s i')).
+  sym_st; apply fold_2 with (eqA:=eqA); auto.
+  Qed.
+
+  End Fold_1.
+  Section Fold_2.
+  Variable i:A.
+
+  Lemma fold_union_inter : forall s s',
+   eqA (fold f (union s s') (fold f (inter s s') i))
+       (fold f s (fold f s' i)).
+  Proof.
+  intros; pattern s; apply set_induction; clear s; intros.
+  trans_st (fold f s' (fold f (inter s s') i)).
+  apply fold_equal; auto with set.
+  trans_st (fold f s' i).
+  apply fold_init; auto.
+  apply fold_1; auto with set.
+  sym_st; apply fold_1; auto.
+  rename s'0 into s''.
+  destruct (In_dec x s').
+  (* In x s' *)   
+  trans_st (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set.
+  apply fold_init; auto.
+  apply fold_2 with (eqA:=eqA); auto with set.
+  rewrite inter_iff; intuition.
+  trans_st (f x (fold f s (fold f s' i))).
+  trans_st (fold f (union s s') (f x (fold f (inter s s') i))).
+  apply fold_equal; auto.
+  apply equal_sym; apply union_Equal with x; auto with set.
+  trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
+  apply fold_commutes; auto.
+  sym_st; apply fold_2 with (eqA:=eqA); auto.
+  (* ~(In x s') *)
+  trans_st (f x (fold f (union s s') (fold f (inter s'' s') i))).
+  apply fold_2 with (eqA:=eqA); auto with set.
+  trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
+  apply Comp;auto.
+  apply fold_init;auto.
+  apply fold_equal;auto.
+  apply equal_sym; apply inter_Add_2 with x; auto with set.
+  trans_st (f x (fold f s (fold f s' i))).
+  sym_st; apply fold_2 with (eqA:=eqA); auto.
+  Qed.
+
+  End Fold_2.
+  Section Fold_3.
+  Variable i:A.
+
+  Lemma fold_diff_inter : forall s s', 
+   eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
+  Proof.
+  intros.
+  trans_st (fold f (union (diff s s') (inter s s')) 
+              (fold f (inter (diff s s') (inter s s')) i)).
+  sym_st; apply fold_union_inter; auto.
+  trans_st (fold f s (fold f (inter (diff s s') (inter s s')) i)).
+  apply fold_equal; auto with set.
+  apply fold_init; auto.
+  apply fold_1; auto with set.
+  Qed.
+
+  Lemma fold_union: forall s s', (forall x, ~In x s\/~In x s') ->
+   eqA (fold f (union s s') i) (fold f s (fold f s' i)).
+  Proof.
+  intros.
+  trans_st (fold f (union s s') (fold f (inter s s') i)).
+  apply fold_init; auto.
+  sym_st; apply fold_1; auto with set.
+  unfold Empty; intro a; generalize (H a); set_iff; tauto.
+  apply fold_union_inter; auto.
+  Qed.
+
+  End Fold_3.
+  End Fold.
+
+  Lemma fold_plus :
+   forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
+  Proof.
+  assert (st := gen_st nat).
+  assert (fe : compat_op E.eq (@eq _) (fun _ => S)) by unfold compat_op; auto. 
+  assert (fp : transpose (@eq _) (fun _:elt => S)) by unfold transpose; auto.
+  intros s p; pattern s; apply set_induction; clear s; intros.
+  rewrite (fold_1 st p (fun _ => S) H).
+  rewrite (fold_1 st 0 (fun _ => S) H); trivial.
+  assert (forall p s', Add x s s' -> fold (fun _ => S) s' p = S (fold (fun _ => S) s p)).
+   change S with ((fun _ => S) x).  
+   intros; apply fold_2; auto.
+  rewrite H2; auto.
+  rewrite (H2 0); auto.
+  rewrite H.
+  simpl; auto.
+  Qed.
+
+  (** properties of [cardinal] *)
+
+  Lemma empty_cardinal : cardinal empty = 0.
+  Proof.
+  rewrite cardinal_fold; apply fold_1; auto.
+  Qed.
+
+  Hint Immediate empty_cardinal cardinal_1 : set.
+
+  Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
+  Proof.
+  intros.
+  rewrite (singleton_equal_add x).
+  replace 0 with (cardinal empty); auto with set.
+  apply cardinal_2 with x; auto with set.
+  Qed.
+
+  Hint Resolve singleton_cardinal: set.
+
+  Lemma diff_inter_cardinal :
+   forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s .
+  Proof.
+  intros; do 3 rewrite cardinal_fold.
+  rewrite <- fold_plus.
+  apply fold_diff_inter with (eqA:=@eq nat); auto.
+  Qed.
+
+  Lemma union_cardinal: 
+   forall s s', (forall x, ~In x s\/~In x s') -> 
+   cardinal (union s s')=cardinal s+cardinal s'.
+  Proof.
+  intros; do 3 rewrite cardinal_fold.
+  rewrite <- fold_plus.
+  apply fold_union; auto.
+  Qed.
+
+  Lemma subset_cardinal : 
+   forall s s', s[<=]s' -> cardinal s <= cardinal s' .
+  Proof.
+  intros.
+  rewrite <- (diff_inter_cardinal s' s).
+  rewrite (inter_sym s' s).
+  rewrite (inter_subset_equal H); auto with arith.
+  Qed.
+
+  Lemma subset_cardinal_lt : 
+   forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.
+  Proof. 
+  intros.
+  rewrite <- (diff_inter_cardinal s' s).
+  rewrite (inter_sym s' s).
+  rewrite (inter_subset_equal H).
+  generalize (@cardinal_inv_1 (diff s' s)).
+  destruct (cardinal (diff s' s)).
+  intro H2; destruct (H2 (refl_equal _) x).
+  set_iff; auto.
+  intros _.
+  change (0 + cardinal s < S n + cardinal s).
+  apply Plus.plus_lt_le_compat; auto with arith.
+  Qed. 
+
+  Theorem union_inter_cardinal :
+   forall s s', cardinal (union s s') + cardinal (inter s s')  = cardinal s  + cardinal s' .
+  Proof.
+  intros.
+  do 4 rewrite cardinal_fold.
+  do 2 rewrite <- fold_plus.
+  apply fold_union_inter with (eqA:=@eq nat); auto.
+  Qed.
+
+  Lemma union_cardinal_inter : 
+   forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
+  Proof.
+  intros.
+  rewrite <- union_inter_cardinal.
+  rewrite Plus.plus_comm.
+  auto with arith.
+  Qed.
+
+  Lemma union_cardinal_le : 
+   forall s s', cardinal (union s s') <= cardinal s  + cardinal s'.
+  Proof.
+   intros; generalize (union_inter_cardinal s s').
+   intros; rewrite <- H; auto with arith.
+  Qed.
+
+  Lemma add_cardinal_1 : 
+   forall s x, In x s -> cardinal (add x s) = cardinal s.
+  Proof.
+  auto with set.  
+  Qed.
+
+  Lemma add_cardinal_2 :
+   forall s x, ~In x s -> cardinal (add x s) = S (cardinal s).
+  Proof.
+  intros.
+  do 2 rewrite cardinal_fold.
+  change S with ((fun _ => S) x);
+   apply fold_add with (eqA:=@eq nat); auto.
+  Qed.
+
+  Lemma remove_cardinal_1 :
+   forall s x, In x s -> S (cardinal (remove x s)) = cardinal s.
+  Proof.
+  intros.
+  do 2 rewrite cardinal_fold.
+  change S with ((fun _ =>S) x).
+  apply remove_fold_1 with (eqA:=@eq nat); auto.
+  Qed.
+
+  Lemma remove_cardinal_2 : 
+   forall s x, ~In x s -> cardinal (remove x s) = cardinal s.
+  Proof. 
+  auto with set.
+  Qed.
+
+  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
+
+End Properties.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index a25b83fc8..726f569d6 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -290,6 +290,149 @@ inversion_clear H1; auto.
 elim H2; auto.
 Qed.
 
+Let addlistA x l l' := forall y, InA y l' <-> eqA x y \/ InA y l.
+
+Lemma removeA_add :
+  forall s s' x x', NoDupA s -> NoDupA (x' :: s') ->
+  ~ eqA x x' -> ~ InA x s -> 
+  addlistA x s (x' :: s') -> addlistA x (removeA x' s) s'.
+Proof.
+unfold addlistA; intros.
+inversion_clear H0.
+rewrite removeA_InA; auto.
+split; intros.
+destruct (eqA_dec x y); auto; intros.
+right; split; auto.
+destruct (H3 y); clear H3.
+destruct H6; intuition.
+swap H4; apply InA_eqA with y; auto.
+destruct H0.
+assert (InA y (x' :: s')) by rewrite H3; auto.
+inversion_clear H6; auto.
+elim H1; apply eqA_trans with y; auto.
+destruct H0.
+assert (InA y (x' :: s')) by rewrite H3; auto.
+inversion_clear H7; auto.
+elim H6; auto.
+Qed.
+
+Section Fold.
+
+Variable B:Set.
+Variable eqB:B->B->Prop.
+
+(** Two-argument functions that allow to reorder its arguments. *)
+Definition transpose (f : A -> B -> B) :=
+  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). 
+
+(** Compatibility of a two-argument function with respect to two equalities. *)
+Definition compat_op (f : A -> B -> B) :=
+  forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
+
+(** Compatibility of a function upon natural numbers. *)
+Definition compat_nat (f : A -> nat) :=
+  forall x x' : A, eqA x x' -> f x = f x'.
+
+Variable st:Setoid_Theory _ eqB.
+Variable f:A->B->B.
+Variable Comp:compat_op f.
+Variable Ass:transpose f.
+Variable i:B.
+
+Lemma removeA_fold_right_0 :
+  forall s x, ~InA x s ->
+  eqB (fold_right f i s) (fold_right f i (removeA x s)).
+Proof.
+ simple induction s; simpl; intros.
+ refl_st.
+ destruct (eqA_dec x a); simpl; intros.
+ absurd_hyp e; auto.
+ apply Comp; auto. 
+Qed.   
+
+Lemma removeA_fold_right :
+  forall s x, NoDupA s -> InA x s ->
+  eqB (fold_right f i s) (f x (fold_right f i (removeA x s))).
+Proof.
+ simple induction s; simpl.  
+ inversion_clear 2.
+ intros.
+ inversion_clear H0.
+ destruct (eqA_dec x a); simpl; intros.
+ apply Comp; auto. 
+ apply removeA_fold_right_0; auto.
+ swap H2; apply InA_eqA with x; auto.
+ inversion_clear H1. 
+ destruct n; auto.
+ trans_st (f a (f x (fold_right f i (removeA x l)))).
+Qed.   
+
+Lemma fold_right_equal :
+  forall s s', NoDupA s -> NoDupA s' ->
+  eqlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
+Proof.
+ simple induction s.
+ destruct s'; simpl.
+ intros; refl_st; auto.
+ unfold eqlistA; intros.
+ destruct (H1 a).
+ assert (X : InA a nil); auto; inversion X.
+ intros x l Hrec s' N N' E; simpl in *.
+ trans_st (f x (fold_right f i (removeA x s'))).
+ apply Comp; auto.
+ apply Hrec; auto.
+ inversion N; auto.
+ apply removeA_NoDupA; auto; apply eqA_trans.
+ apply removeA_eqlistA; auto.
+ inversion_clear N; auto.
+ sym_st.
+ apply removeA_fold_right; auto.
+ unfold eqlistA in E.
+ rewrite <- E; auto.
+Qed.
+
+Lemma fold_right_add :
+  forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
+  addlistA x s s' -> eqB (fold_right f i s') (f x (fold_right f i s)).
+Proof.   
+ simple induction s'.
+ unfold addlistA; intros.
+ destruct (H2 x); clear H2.
+ assert (X : InA x nil); auto; inversion X.
+ intros x' l' Hrec s x N N' IN EQ; simpl.
+ (* if x=x' *)
+ destruct (eqA_dec x x').
+ apply Comp; auto.
+ apply fold_right_equal; auto.
+ inversion_clear N'; trivial.
+ unfold eqlistA; unfold addlistA in EQ; intros.
+ destruct (EQ x0); clear EQ.
+ split; intros.
+ destruct H; auto.
+ inversion_clear N'.
+ destruct H2; apply InA_eqA with x0; auto.
+ apply eqA_trans with x; auto.
+ assert (X:InA x0 (x' :: l')); auto; inversion_clear X; auto.
+ destruct IN; apply InA_eqA with x0; auto.
+ apply eqA_trans with x'; auto.
+ (* else x<>x' *)   
+ trans_st (f x' (f x (fold_right f i (removeA x' s)))).
+ apply Comp; auto.
+ apply Hrec; auto.
+ apply removeA_NoDupA; auto; apply eqA_trans.
+ inversion_clear N'; auto.
+ rewrite removeA_InA; intuition.
+ apply removeA_add; auto.
+ trans_st (f x (f x' (fold_right f i (removeA x' s)))).
+ apply Comp; auto.
+ sym_st.
+ apply removeA_fold_right; auto.
+ destruct (EQ x'). 
+ destruct H; auto; destruct n; auto.
+Qed.
+
+End Fold.
+
 End Remove.
 
 End Type_with_equality.
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 3bf86eb48..9496099a8 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -662,3 +662,26 @@ Implicit Arguments Setoid_Theory [].
 Implicit Arguments Seq_refl [].
 Implicit Arguments Seq_sym [].
 Implicit Arguments Seq_trans [].
+
+
+(* Some tactics for manipulating Setoid Theory not officially 
+   declared as Setoid. *)
+
+Ltac trans_st x := match goal with 
+  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+     apply (Seq_trans _ _ H) with x; auto
+ end.
+
+Ltac sym_st := match goal with 
+  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+     apply (Seq_sym _ _ H); auto
+ end.
+
+Ltac refl_st := match goal with 
+  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+     apply (Seq_refl _ _ H); auto
+ end.
+
+Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A).
+Proof. constructor; congruence. Qed.
+