23 files changed, 205 insertions, 173 deletions

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index e6755898..5f686099 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Classical_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
@@ -56,7 +56,7 @@ Section Ensembles_classical.
     forall X Y:Ensemble U,
       Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
   Proof.
-    intros X Y I NI. 
+    intros X Y I NI.
     elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
     intros x YX.
     apply Inhabited_intro with x.
@@ -78,7 +78,7 @@ Section Ensembles_classical.
     unfold Subtract at 1 in |- *; auto with sets.
   Qed.
   Hint Resolve Subtract_intro : sets.
-  
+
   Lemma Subtract_inv :
     forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
   Proof.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index ad81316d..0719365f 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -24,13 +24,13 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Constructive_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Ensembles.
 
 Section Ensembles_facts.
   Variable U : Type.
-  
+
   Lemma Extension : forall B C:Ensemble U, B = C -> Same_set U B C.
   Proof.
     intros B C H'; rewrite H'; auto with sets.
@@ -52,7 +52,7 @@ Section Ensembles_facts.
   Proof.
     unfold Add at 1 in |- *; auto with sets.
   Qed.
-  
+
   Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
   Proof.
     unfold Add at 1 in |- *; auto with sets.
@@ -98,15 +98,15 @@ Section Ensembles_facts.
   Proof.
     intros B C x H'; elim H'; auto with sets.
   Qed.
-  
+
   Lemma Add_inv :
     forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
   Proof.
-    intros A x y H'; induction H'. 
+    intros A x y H'; induction H'.
       left; assumption.
       right; apply Singleton_inv; assumption.
   Qed.
-  
+
   Lemma Intersection_inv :
     forall (B C:Ensemble U) (x:U),
       In U (Intersection U B C) x -> In U B x /\ In U C x.
@@ -125,7 +125,7 @@ Section Ensembles_facts.
   Proof.
     unfold Setminus at 1 in |- *; red in |- *; auto with sets.
   Qed.
- 
+
   Lemma Strict_Included_intro :
     forall X Y:Ensemble U, Included U X Y /\ X <> Y -> Strict_Included U X Y.
   Proof.
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 1e1b70d5..8c69e687 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Cpo.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
@@ -35,7 +35,7 @@ Section Bounds.
   Variable D : PO U.
 
   Let C := Carrier_of U D.
-  
+
   Let R := Rel_of U D.
 
   Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
@@ -45,7 +45,7 @@ Section Bounds.
   Inductive Lower_Bound (B:Ensemble U) (x:U) : Prop :=
     Lower_Bound_definition :
     In U C x -> (forall y:U, In U B y -> R x y) -> Lower_Bound B x.
-  
+
   Inductive Lub (B:Ensemble U) (x:U) : Prop :=
     Lub_definition :
     Upper_Bound B x -> (forall y:U, Upper_Bound B y -> R x y) -> Lub B x.
@@ -57,7 +57,7 @@ Section Bounds.
   Inductive Bottom (bot:U) : Prop :=
     Bottom_definition :
     In U C bot -> (forall y:U, In U C y -> R bot y) -> Bottom bot.
-  
+
   Inductive Totally_ordered (B:Ensemble U) : Prop :=
     Totally_ordered_definition :
     (Included U B C ->
@@ -77,7 +77,7 @@ Section Bounds.
       Included U (Couple U x1 x2) X ->
       exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
     Directed X.
-  
+
   Inductive Complete : Prop :=
     Definition_of_Complete :
     (exists bot : _, Bottom bot) ->
@@ -102,7 +102,7 @@ Section Specific_orders.
 
   Record Cpo : Type := Definition_of_cpo
     {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
-  
+
   Record Chain : Type := Definition_of_chain
     {PO_of_chain : PO U;
     Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index c38a2fe1..0fa9c74a 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -24,27 +24,27 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Ensembles.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Section Ensembles.
   Variable U : Type.
-  
-  Definition Ensemble := U -> Prop. 
+
+  Definition Ensemble := U -> Prop.
 
   Definition In (A:Ensemble) (x:U) : Prop := A x.
-  
+
   Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x.
-  
+
   Inductive Empty_set : Ensemble :=.
-  
+
   Inductive Full_set : Ensemble :=
     Full_intro : forall x:U, In Full_set x.
 
-(** NB: The following definition builds-in equality of elements in [U] as 
-     Leibniz equality. 
+(** NB: The following definition builds-in equality of elements in [U] as
+     Leibniz equality.
 
-     This may have to be changed if we replace [U] by a Setoid on [U] 
-     with its own equality [eqs], with  
+     This may have to be changed if we replace [U] by a Setoid on [U]
+     with its own equality [eqs], with
      [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
 
   Inductive Singleton (x:U) : Ensemble :=
@@ -55,7 +55,7 @@ Section Ensembles.
     | Union_intror : forall x:U, In C x -> In (Union B C) x.
 
   Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x).
-  
+
   Inductive Intersection (B C:Ensemble) : Ensemble :=
     Intersection_intro :
     forall x:U, In B x -> In C x -> In (Intersection B C) x.
@@ -63,29 +63,29 @@ Section Ensembles.
   Inductive Couple (x y:U) : Ensemble :=
     | Couple_l : In (Couple x y) x
     | Couple_r : In (Couple x y) y.
-  
+
   Inductive Triple (x y z:U) : Ensemble :=
     | Triple_l : In (Triple x y z) x
     | Triple_m : In (Triple x y z) y
     | Triple_r : In (Triple x y z) z.
-  
+
   Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x.
-  
+
   Definition Setminus (B C:Ensemble) : Ensemble :=
     fun x:U => In B x /\ ~ In C x.
-  
+
   Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x).
-  
+
   Inductive Disjoint (B C:Ensemble) : Prop :=
     Disjoint_intro : (forall x:U, ~ In (Intersection B C) x) -> Disjoint B C.
 
   Inductive Inhabited (B:Ensemble) : Prop :=
     Inhabited_intro : forall x:U, In B x -> Inhabited B.
-  
+
   Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C.
-  
+
   Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B.
-  
+
   (** Extensionality Axiom *)
 
   Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index f5eae4ed..019c25a5 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Import Ensembles.
 
@@ -52,7 +52,7 @@ Require Import Constructive_sets.
 
 Section Ensembles_finis_facts.
   Variable U : Type.
-  
+
   Lemma cardinal_invert :
     forall (X:Ensemble U) (p:nat),
       cardinal U X p ->
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 91717f9e..fdcc4150 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
@@ -72,7 +72,7 @@ Section Finite_sets_facts.
   Proof.
     intros X Y H; induction H as [|A Fin_A Hind x].
     rewrite (Empty_set_zero U Y). trivial.
-    intros. 
+    intros.
     rewrite (Union_commutative U (Add U A x) Y).
     rewrite <- (Union_add U Y A x).
     rewrite (Union_commutative U Y A).
@@ -98,7 +98,7 @@ Section Finite_sets_facts.
   Proof.
     intros A H' X; apply Finite_downward_closed with A; auto with sets.
   Qed.
-  
+
   Lemma cardinalO_empty :
     forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
   Proof.
@@ -212,7 +212,7 @@ Section Finite_sets_facts.
   Proof.
     intros; apply cardinal_is_functional with X X; auto with sets.
   Qed.
-  
+
   Lemma card_Add_gen :
     forall (A:Ensemble U) (x:U) (n n':nat),
       cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
@@ -279,7 +279,7 @@ Section Finite_sets_facts.
     intro E; rewrite E; auto with sets arith.
     apply cardinal_unicity with X; auto with sets arith.
   Qed.
-  
+
   Lemma G_aux :
     forall P:Ensemble U -> Prop,
       (forall X:Ensemble U,
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index d3591acf..64c341bd 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Image.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
@@ -40,10 +40,10 @@ Require Export Finite_sets_facts.
 
 Section Image.
   Variables U V : Type.
-  
+
   Inductive Im (X:Ensemble U) (f:U -> V) : Ensemble V :=
     Im_intro : forall x:U, In _ X x -> forall y:V, y = f x -> In _ (Im X f) y.
-  
+
   Lemma Im_def :
     forall (X:Ensemble U) (f:U -> V) (x:U), In _ X x -> In _ (Im X f) (f x).
   Proof.
@@ -62,13 +62,13 @@ Section Image.
     rewrite H0.
     elim Add_inv with U X x x1; auto using Im_def with sets.
     destruct 1; auto using Im_def with sets.
-    elim Add_inv with V (Im X f) (f x) x0. 
+    elim Add_inv with V (Im X f) (f x) x0.
     destruct 1 as [x0 H y H0].
     rewrite H0; auto using Im_def with sets.
     destruct 1; auto using Im_def with sets.
     trivial.
   Qed.
-  
+
   Lemma image_empty : forall f:U -> V, Im (Empty_set U) f = Empty_set V.
   Proof.
     intro f; try assumption.
@@ -88,7 +88,7 @@ Section Image.
     rewrite (Im_add A x f); auto with sets.
     apply Add_preserves_Finite; auto with sets.
   Qed.
-  
+
   Lemma Im_inv :
     forall (X:Ensemble U) (f:U -> V) (y:V),
       In _ (Im X f) y ->  exists x : U, In _ X x /\ f x = y.
@@ -97,9 +97,9 @@ Section Image.
     intros x H'0 y0 H'1; rewrite H'1.
     exists x; auto with sets.
   Qed.
-  
+
   Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.
-  
+
   Lemma not_injective_elim :
     forall f:U -> V,
       ~ injective f ->  exists x : _, (exists y : _, f x = f y /\ x <> y).
@@ -115,7 +115,7 @@ Section Image.
     destruct 1 as [y D]; exists y.
     apply imply_to_and; trivial with sets.
   Qed.
-  
+
   Lemma cardinal_Im_intro :
     forall (A:Ensemble U) (f:U -> V) (n:nat),
       cardinal _ A n ->  exists p : nat, cardinal _ (Im A f) p.
@@ -124,7 +124,7 @@ Section Image.
     apply finite_cardinal; apply finite_image.
     apply cardinal_finite with n; trivial with sets.
   Qed.
-  
+
   Lemma In_Image_elim :
     forall (A:Ensemble U) (f:U -> V),
       injective f -> forall x:U, In _ (Im A f) (f x) -> In _ A x.
@@ -134,7 +134,7 @@ Section Image.
     intros z C; elim C; intros InAz E.
     elim (H z x E); trivial with sets.
   Qed.
-  
+
   Lemma injective_preserves_cardinal :
     forall (A:Ensemble U) (f:U -> V) (n:nat),
       injective f ->
@@ -158,7 +158,7 @@ Section Image.
     red in |- *; intro; apply H'2.
     apply In_Image_elim with f; trivial with sets.
   Qed.
-  
+
   Lemma cardinal_decreases :
     forall (A:Ensemble U) (f:U -> V) (n:nat),
       cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' <= n.
@@ -188,7 +188,7 @@ Section Image.
     apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
       trivial with sets.
   Qed.
-  
+
   Lemma Pigeonhole_principle :
     forall (A:Ensemble U) (f:U -> V) (n:nat),
       cardinal _ A n ->
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index ae2143c8..b63ec1d4 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Infinite_sets.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
@@ -50,7 +50,7 @@ Hint Resolve Defn_of_Approximant.
 
 Section Infinite_sets.
   Variable U : Type.
-  
+
   Lemma make_new_approximant :
     forall A X:Ensemble U,
       ~ Finite U A -> Approximant U A X -> Inhabited U (Setminus U A X).
@@ -61,7 +61,7 @@ Section Infinite_sets.
     red in |- *; intro H'3; apply H'.
     rewrite <- H'3; auto with sets.
   Qed.
-  
+
   Lemma approximants_grow :
     forall A X:Ensemble U,
       ~ Finite U A ->
@@ -101,7 +101,7 @@ Section Infinite_sets.
     apply Defn_of_Approximant; auto with sets.
     apply cardinal_finite with (n := S n0); auto with sets.
   Qed.
-  
+
   Lemma approximants_grow' :
     forall A X:Ensemble U,
       ~ Finite U A ->
@@ -121,7 +121,7 @@ Section Infinite_sets.
     apply cardinal_finite with (n := S n); auto with sets.
     apply approximants_grow with (X := X); auto with sets.
   Qed.
-  
+
   Lemma approximant_can_be_any_size :
     forall A X:Ensemble U,
       ~ Finite U A ->
@@ -135,7 +135,7 @@ Section Infinite_sets.
   Qed.
 
   Variable V : Type.
-  
+
   Theorem Image_set_continuous :
     forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
       Finite V X ->
@@ -230,7 +230,7 @@ Section Infinite_sets.
     rewrite H'4; auto with sets.
     elim H'3; auto with sets.
   Qed.
-  
+
   Theorem Pigeonhole_ter :
     forall (A:Ensemble U) (f:U -> V) (n:nat),
       injective U V f -> Finite V (Im U V A f) -> Finite U A.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 1786edf1..15c1b665 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Integers.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
@@ -45,7 +45,7 @@ Require Export Partial_Order.
 Require Export Cpo.
 
 Section Integers_sect.
-  
+
   Inductive Integers : Ensemble nat :=
     Integers_defn : forall x:nat, In nat Integers x.
 
@@ -53,7 +53,7 @@ Section Integers_sect.
   Proof.
     red in |- *; auto with arith.
   Qed.
-  
+
   Lemma le_antisym : Antisymmetric nat le.
   Proof.
     red in |- *; intros x y H H'; rewrite (le_antisym x y); auto.
@@ -63,12 +63,12 @@ Section Integers_sect.
   Proof.
     red in |- *; intros; apply le_trans with y; auto.
   Qed.
-  
+
   Lemma le_Order : Order nat le.
   Proof.
-    split; [exact le_reflexive | exact le_trans | exact le_antisym]. 
+    split; [exact le_reflexive | exact le_trans | exact le_antisym].
   Qed.
-  
+
   Lemma triv_nat : forall n:nat, In nat Integers n.
   Proof.
     exact Integers_defn.
@@ -77,11 +77,11 @@ Section Integers_sect.
   Definition nat_po : PO nat.
     apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le);
       auto with sets arith.
-    apply Inhabited_intro with (x := 0). 
+    apply Inhabited_intro with (x := 0).
       apply Integers_defn.
-      exact le_Order.
+    exact le_Order.
   Defined.
-  
+
   Lemma le_total_order : Totally_ordered nat nat_po Integers.
   Proof.
     apply Totally_ordered_definition.
@@ -92,7 +92,7 @@ Section Integers_sect.
     intro H'1; right.
     cut (y <= x); auto with sets arith.
   Qed.
-  
+
   Lemma Finite_subset_has_lub :
     forall X:Ensemble nat,
       Finite nat X ->  exists m : nat, Upper_Bound nat nat_po X m.
@@ -124,7 +124,7 @@ Section Integers_sect.
     apply H'4 with (y := x0). elim H'3; simpl in |- *; auto with sets arith. trivial.
     intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial.
     exists x0.
-    apply Upper_Bound_definition. 
+    apply Upper_Bound_definition.
       unfold nat_po. simpl. apply triv_nat.
     intros y H'1; elim H'1.
     intros x1 H'4; try assumption.
@@ -148,7 +148,7 @@ Section Integers_sect.
     absurd (S x <= x); auto with arith.
     apply triv_nat.
  Qed.
-  
+
   Lemma Integers_infinite : ~ Finite nat Integers.
   Proof.
     generalize Integers_has_no_ub.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index d2bff488..7216ae33 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Multiset.v 10616 2008-03-04 17:33:35Z letouzey $ i*)
+(*i $Id$ i*)
 
 (* G. Huet 1-9-95 *)
 
-Require Import Permut.
+Require Import Permut Setoid.
 
 Set Implicit Arguments.
 
@@ -18,11 +18,12 @@ Section multiset_defs.
 
   Variable A : Type.
   Variable eqA : A -> A -> Prop.
+  Hypothesis eqA_equiv : Equivalence eqA.
   Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
   Inductive multiset : Type :=
     Bag : (A -> nat) -> multiset.
-  
+
   Definition EmptyBag := Bag (fun a:A => 0).
   Definition SingletonBag (a:A) :=
     Bag (fun a':A => match Aeq_dec a a' with
@@ -31,23 +32,23 @@ Section multiset_defs.
                      end).
 
   Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a.
-  
+
   (** multiset equality *)
   Definition meq (m1 m2:multiset) :=
     forall a:A, multiplicity m1 a = multiplicity m2 a.
-  
+
   Lemma meq_refl : forall x:multiset, meq x x.
   Proof.
     destruct x; unfold meq; reflexivity.
   Qed.
-  
+
   Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.
   Proof.
     unfold meq in |- *.
     destruct x; destruct y; destruct z.
     intros; rewrite H; auto.
   Qed.
-  
+
   Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.
   Proof.
     unfold meq in |- *.
@@ -62,7 +63,7 @@ Section multiset_defs.
   Proof.
     unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
   Qed.
-  
+
   Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
   Proof.
     unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
@@ -70,7 +71,7 @@ Section multiset_defs.
 
 
   Require Plus. (* comm. and ass. of plus *)
-  
+
   Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
   Proof.
     unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.
@@ -106,28 +107,28 @@ Section multiset_defs.
   Lemma munion_rotate :
     forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).
   Proof.
-    intros; apply (op_rotate multiset munion meq). 
+    intros; apply (op_rotate multiset munion meq).
       apply munion_comm.
       apply munion_ass.
       exact meq_trans.
       exact meq_sym.
       trivial.
   Qed.
-  
+
   Lemma meq_congr :
     forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).
   Proof.
     intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right.
       exact meq_trans.
   Qed.
-  
+
   Lemma munion_perm_left :
     forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).
   Proof.
     intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym.
       exact meq_trans.
   Qed.
-  
+
   Lemma multiset_twist1 :
     forall x y z t:multiset,
       meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z).
@@ -156,7 +157,7 @@ Section multiset_defs.
     apply meq_right; apply meq_left; trivial.
     apply multiset_twist1.
   Qed.
-  
+
   Lemma treesort_twist2 :
     forall x y z t u:multiset,
       meq u (munion y z) ->
@@ -167,8 +168,17 @@ Section multiset_defs.
     apply multiset_twist2.
   Qed.
 
+  (** SingletonBag *)
+
+  Lemma meq_singleton : forall a a',
+    eqA a a' -> meq (SingletonBag a) (SingletonBag a').
+  Proof.
+    intros; red; simpl; intro a0.
+    destruct (Aeq_dec a a0) as [Ha|Ha]; rewrite H in Ha;
+      decide (Aeq_dec a' a0) with Ha; reflexivity.
+  Qed.
 
-(*i theory of minter to do similarly 
+(*i theory of minter to do similarly
 Require Min.
 (* multiset intersection *)
 Definition minter := [m1,m2:multiset]
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 6210913c..4fe8f4f6 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -24,27 +24,27 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Partial_Order.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
 
 Section Partial_orders.
   Variable U : Type.
-  
+
   Definition Carrier := Ensemble U.
-  
+
   Definition Rel := Relation U.
-  
+
   Record PO : Type := Definition_of_PO
     { Carrier_of : Ensemble U;
       Rel_of : Relation U;
       PO_cond1 : Inhabited U Carrier_of;
       PO_cond2 : Order U Rel_of }.
   Variable p : PO.
-  
+
   Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y.
-  
+
   Inductive covers (y x:U) : Prop :=
     Definition_of_covers :
     Strict_Rel_of x y ->
@@ -60,7 +60,7 @@ Hint Resolve Definition_of_covers: sets v62.
 Section Partial_order_facts.
   Variable U : Type.
   Variable D : PO U.
-  
+
   Lemma Strict_Rel_Transitive_with_Rel :
     forall x y z:U,
       Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 4380f10c..f593031a 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Permut.v 10616 2008-03-04 17:33:35Z letouzey $ i*)
+(*i $Id$ i*)
 
 (* G. Huet 1-9-95 *)
 
@@ -36,23 +36,23 @@ Section Axiomatisation.
     apply cong_left; trivial.
     apply cong_right; trivial.
   Qed.
-  
+
   Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)).
   Proof.
     intros; apply cong_right; apply op_comm.
   Qed.
-  
+
   Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z).
   Proof.
     intros; apply cong_left; apply op_comm.
   Qed.
-  
+
   Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y).
   Proof.
     intros.
     apply cong_trans with (op x (op y z)).
     apply op_ass.
-    apply cong_trans with (op x (op z y)). 
+    apply cong_trans with (op x (op z y)).
     apply cong_right; apply op_comm.
     apply cong_sym; apply op_ass.
   Qed.
@@ -66,7 +66,7 @@ Section Axiomatisation.
     apply cong_left; apply op_comm.
     apply op_ass.
   Qed.
-  
+
   Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)).
   Proof.
     intros; apply cong_trans with (op (op x y) z).
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index c9a52ac2..c323ca35 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 34c49409..36d2150c 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset_Classical_facts.v 10855 2008-04-27 11:16:15Z msozeau $ i*)
+(*i $Id$ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
@@ -40,7 +40,7 @@ Require Export Classical_sets.
 Section Sets_as_an_algebra.
 
   Variable U : Type.
-  
+
   Lemma sincl_add_x :
     forall (A B:Ensemble U) (x:U),
       ~ In U A x ->
@@ -63,7 +63,7 @@ Section Sets_as_an_algebra.
     intros X x H'; red in |- *.
     intros x0 H'0; elim H'0; auto with sets.
   Qed.
-  
+
   Lemma incl_soustr :
     forall (X Y:Ensemble U) (x:U),
       Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
@@ -73,7 +73,7 @@ Section Sets_as_an_algebra.
     intros H'1 H'2.
     apply Subtract_intro; auto with sets.
   Qed.
-  
+
   Lemma incl_soustr_add_l :
     forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
   Proof.
@@ -93,7 +93,7 @@ Section Sets_as_an_algebra.
     red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
   Qed.
   Hint Resolve incl_soustr_add_r: sets v62.
-  
+
   Lemma add_soustr_2 :
     forall (X:Ensemble U) (x:U),
       In U X x -> Included U X (Add U (Subtract U X x) x).
@@ -103,7 +103,7 @@ Section Sets_as_an_algebra.
     elim (classic (x = x0)); intro K; auto with sets.
     elim K; auto with sets.
   Qed.
-  
+
   Lemma add_soustr_1 :
     forall (X:Ensemble U) (x:U),
       In U X x -> Included U (Add U (Subtract U X x) x) X.
@@ -114,7 +114,7 @@ Section Sets_as_an_algebra.
     intros t H'1; try assumption.
     rewrite <- (Singleton_inv U x t); auto with sets.
   Qed.
-  
+
   Lemma add_soustr_xy :
     forall (X:Ensemble U) (x y:U),
       x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
@@ -133,7 +133,7 @@ Section Sets_as_an_algebra.
     intro H'0; elim H'0; auto with sets.
     intro H'0; rewrite <- H'0; auto with sets.
   Qed.
-  
+
   Lemma incl_st_add_soustr :
     forall (X Y:Ensemble U) (x:U),
       ~ In U X x ->
@@ -151,13 +151,13 @@ Section Sets_as_an_algebra.
     red in |- *; intro H'0; apply H'2.
     rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
   Qed.
-  
+
   Lemma Sub_Add_new :
     forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
   Proof.
     auto using incl_soustr_add_l with sets.
   Qed.
-  
+
   Lemma Simplify_add :
     forall (X X0:Ensemble U) (x:U),
       ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
@@ -167,7 +167,7 @@ Section Sets_as_an_algebra.
     rewrite (Sub_Add_new X0 x); auto with sets.
     rewrite H'1; auto with sets.
   Qed.
-  
+
   Lemma Included_Add :
     forall (X A:Ensemble U) (x:U),
       Included U X (Add U A x) ->
@@ -201,7 +201,7 @@ Section Sets_as_an_algebra.
     absurd (In U X x0); auto with sets.
     rewrite <- H'5; auto with sets.
   Qed.
-  
+
   Lemma setcover_inv :
     forall A x y:Ensemble U,
       covers (Ensemble U) (Power_set_PO U A) y x ->
@@ -219,7 +219,7 @@ Section Sets_as_an_algebra.
     elim H'1.
     exists z; auto with sets.
   Qed.
-  
+
   Theorem Add_covers :
     forall A a:Ensemble U,
       Included U a A ->
@@ -255,7 +255,7 @@ Section Sets_as_an_algebra.
     intros x1 H'10; elim H'10; auto with sets.
     intros x2 H'11; elim H'11; auto with sets.
   Qed.
-  
+
   Theorem covers_Add :
     forall A a a':Ensemble U,
       Included U a A ->
@@ -301,7 +301,7 @@ Section Sets_as_an_algebra.
     intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.
     apply Add_covers; intuition.
   Qed.
-  
+
   Theorem Singleton_atomic :
     forall (x:U) (A:Ensemble U),
       In U A x ->
@@ -311,7 +311,7 @@ Section Sets_as_an_algebra.
     rewrite <- (Empty_set_zero' U x).
     apply Add_covers; auto with sets.
   Qed.
-  
+
   Lemma less_than_singleton :
     forall (X:Ensemble U) (x:U),
       Strict_Included U X (Singleton U x) -> X = Empty_set U.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index edb6a215..76f7f1ec 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
@@ -41,34 +41,34 @@ Section Sets_as_an_algebra.
   Proof.
     auto 6 with sets.
   Qed.
-  
+
   Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
   Proof.
     unfold Add at 1 in |- *; auto using Empty_set_zero with sets.
   Qed.
-  
+
   Lemma less_than_empty :
     forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
   Proof.
     auto with sets.
   Qed.
-  
+
   Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.
   Proof.
     auto with sets.
   Qed.
-  
+
   Theorem Union_associative :
     forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
   Proof.
     auto 9 with sets.
   Qed.
-  
+
   Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.
   Proof.
     auto 7 with sets.
   Qed.
-  
+
   Lemma Union_absorbs :
     forall A B:Ensemble U, Included U B A -> Union U A B = A.
   Proof.
@@ -82,7 +82,7 @@ Section Sets_as_an_algebra.
     intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
     intros x0 H'; elim H'; auto with sets.
   Qed.
-  
+
   Theorem Triple_as_union :
     forall x y z:U,
       Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
@@ -94,7 +94,7 @@ Section Sets_as_an_algebra.
     intros x1 H'0; elim H'0; auto with sets.
     intros x0 H'; elim H'; auto with sets.
   Qed.
-  
+
   Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
   Proof.
     intros x y.
@@ -102,7 +102,7 @@ Section Sets_as_an_algebra.
     rewrite <- (Union_idempotent (Singleton U x)).
     apply Triple_as_union.
   Qed.
-  
+
   Theorem Triple_as_Couple_Singleton :
     forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
   Proof.
@@ -110,7 +110,7 @@ Section Sets_as_an_algebra.
     rewrite <- (Triple_as_union x y z).
     rewrite <- (Couple_as_union x y); auto with sets.
   Qed.
-  
+
   Theorem Intersection_commutative :
     forall A B:Ensemble U, Intersection U A B = Intersection U B A.
   Proof.
@@ -118,7 +118,7 @@ Section Sets_as_an_algebra.
     apply Extensionality_Ensembles.
     split; red in |- *; intros x H'; elim H'; auto with sets.
   Qed.
-  
+
   Theorem Distributivity :
     forall A B C:Ensemble U,
       Intersection U A (Union U B C) =
@@ -132,7 +132,7 @@ Section Sets_as_an_algebra.
     elim H'1; auto with sets.
     elim H'; intros x0 H'0; elim H'0; auto with sets.
   Qed.
-  
+
   Theorem Distributivity' :
     forall A B C:Ensemble U,
       Union U A (Intersection U B C) =
@@ -149,13 +149,13 @@ Section Sets_as_an_algebra.
     generalize H'1.
     elim H'2; auto with sets.
   Qed.
-  
+
   Theorem Union_add :
     forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
   Proof.
     unfold Add in |- *; auto using Union_associative with sets.
   Qed.
-  
+
   Theorem Non_disjoint_union :
     forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
   Proof.
@@ -165,7 +165,7 @@ Section Sets_as_an_algebra.
     intros x0 H'0; elim H'0; auto with sets.
     intros t H'1; elim H'1; auto with sets.
   Qed.
-  
+
   Theorem Non_disjoint_union' :
     forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
   Proof.
@@ -178,12 +178,12 @@ Section Sets_as_an_algebra.
     lapply (Singleton_inv U x x0); auto with sets.
     intro H'4; apply H'; rewrite H'4; auto with sets.
   Qed.
-  
+
   Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
   Proof.
     intro x; rewrite (Empty_set_zero' x); auto with sets.
   Qed.
-  
+
   Lemma incl_add :
     forall (A B:Ensemble U) (x:U),
       Included U A B -> Included U (Add U A x) (Add U B x).
@@ -209,7 +209,7 @@ Section Sets_as_an_algebra.
     absurd (In U A x0); auto with sets.
     rewrite <- H'4; auto with sets.
   Qed.
-  
+
   Lemma Add_commutative :
     forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
   Proof.
@@ -220,7 +220,7 @@ Section Sets_as_an_algebra.
     rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
       auto with sets.
   Qed.
-  
+
   Lemma Add_commutative' :
     forall (A:Ensemble U) (x y z:U),
       Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.
@@ -229,7 +229,7 @@ Section Sets_as_an_algebra.
     rewrite (Add_commutative (Add U A x) y z).
     rewrite (Add_commutative A x z); auto with sets.
   Qed.
-  
+
   Lemma Add_distributes :
     forall (A B:Ensemble U) (x y:U),
       Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 64c4c654..85d0cffc 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -24,42 +24,42 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_1.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
 
 Section Relations_1.
    Variable U : Type.
-   
+
    Definition Relation := U -> U -> Prop.
    Variable R : Relation.
-   
+
    Definition Reflexive : Prop := forall x:U, R x x.
-   
+
    Definition Transitive : Prop := forall x y z:U, R x y -> R y z -> R x z.
-   
+
    Definition Symmetric : Prop := forall x y:U, R x y -> R y x.
-   
+
    Definition Antisymmetric : Prop := forall x y:U, R x y -> R y x -> x = y.
-   
+
    Definition contains (R R':Relation) : Prop :=
      forall x y:U, R' x y -> R x y.
-   
+
    Definition same_relation (R R':Relation) : Prop :=
      contains R R' /\ contains R' R.
-   
+
    Inductive Preorder : Prop :=
        Definition_of_preorder : Reflexive -> Transitive -> Preorder.
-   
+
    Inductive Order : Prop :=
        Definition_of_order :
          Reflexive -> Transitive -> Antisymmetric -> Order.
-   
+
    Inductive Equivalence : Prop :=
        Definition_of_equivalence :
          Reflexive -> Transitive -> Symmetric -> Equivalence.
-   
+
    Inductive PER : Prop :=
        Definition_of_PER : Symmetric -> Transitive -> PER.
-   
+
 End Relations_1.
 Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
   same_relation: sets v62.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index 6ee7f5e2..fd83b0e0 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_1_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Relations_1.
 
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index a74102fd..11ac85e8 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_2.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Relations_1.
 
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 2374c2bf..3554901b 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_2_facts.v 10637 2008-03-07 23:52:56Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Export Relations_1.
 Require Export Relations_1_facts.
@@ -140,7 +140,7 @@ intros U R H' x b H'0; elim H'0.
 intros x0 a H'1; exists a; auto with sets.
 intros x0 y z H'1 H'2 H'3 a H'4.
 red in H'.
-specialize H' with (x := x0) (a := a) (b := y); lapply H'; 
+specialize H' with (x := x0) (a := a) (b := y); lapply H';
  [ intro H'8; lapply H'8;
     [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ]
  | clear H' ]; auto with sets.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index b8c65148..970db182 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_3.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Relations_1.
 Require Export Relations_2.
@@ -32,26 +32,26 @@ Require Export Relations_2.
 Section Relations_3.
    Variable U : Type.
    Variable R : Relation U.
-   
+
    Definition coherent (x y:U) : Prop :=
       exists z : _, Rstar U R x z /\ Rstar U R y z.
-   
+
    Definition locally_confluent (x:U) : Prop :=
      forall y z:U, R x y -> R x z -> coherent y z.
-   
+
    Definition Locally_confluent : Prop := forall x:U, locally_confluent x.
-   
+
    Definition confluent (x:U) : Prop :=
      forall y z:U, Rstar U R x y -> Rstar U R x z -> coherent y z.
-   
+
    Definition Confluent : Prop := forall x:U, confluent x.
-   
+
    Inductive noetherian (x: U) : Prop :=
        definition_of_noetherian :
          (forall y:U, R x y -> noetherian y) -> noetherian x.
-   
+
    Definition Noetherian : Prop := forall x:U, noetherian x.
-   
+
 End Relations_3.
 Hint Unfold coherent: sets v62.
 Hint Unfold locally_confluent: sets v62.
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 38ff9eae..d8bf7dc3 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_3_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
 
 Require Export Relations_1.
 Require Export Relations_1_facts.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 42c96191..909c7983 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Uniset.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** Sets as characteristic functions *)
 
@@ -90,10 +90,10 @@ Qed.
 Definition union (m1 m2:uniset) :=
   Charac (fun a:A => orb (charac m1 a) (charac m2 a)).
 
-Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).  
-Proof.  
-unfold seq in |- *; unfold union in |- *; simpl in |- *; auto.  
-Qed. 
+Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).
+Proof.
+unfold seq in |- *; unfold union in |- *; simpl in |- *; auto.
+Qed.
 Hint Resolve union_empty_left.
 
 Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
@@ -203,7 +203,7 @@ apply uniset_twist2.
 Qed.
 
 
-(*i theory of minter to do similarly 
+(*i theory of minter to do similarly
 Require Min.
 (* uniset intersection *)
 Definition minter := [m1,m2:uniset]
diff --git a/theories/Sets/vo.itarget b/theories/Sets/vo.itarget
new file mode 100644
index 00000000..9ebe92f5
--- /dev/null
+++ b/theories/Sets/vo.itarget
@@ -0,0 +1,22 @@
+Classical_sets.vo
+Constructive_sets.vo
+Cpo.vo
+Ensembles.vo
+Finite_sets_facts.vo
+Finite_sets.vo
+Image.vo
+Infinite_sets.vo
+Integers.vo
+Multiset.vo
+Partial_Order.vo
+Permut.vo
+Powerset_Classical_facts.vo
+Powerset_facts.vo
+Powerset.vo
+Relations_1_facts.vo
+Relations_1.vo
+Relations_2_facts.vo
+Relations_2.vo
+Relations_3_facts.vo
+Relations_3.vo
+Uniset.vo