Merge SetoidList2 into SetoidList.

This file contains low-level stuff for FSets/FMaps. Switching it to
the new version (the one using Equivalence and so on instead of
eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in
FSets/FMaps that are minor and probably invisible to standard users.

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

17 files changed, 697 insertions, 1441 deletions

diff --git a/Makefile.common b/Makefile.common
index 532fe9b3d..967f7b21e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -356,7 +356,7 @@ QARITHVO:=$(addprefix theories/QArith/, \
 
 LISTSVO:=$(addprefix theories/Lists/, \
  ListSet.vo   	Streams.vo 	StreamMemo.vo  \
- TheoryList.vo	List.vo 	SetoidList.vo  SetoidList2.vo \
+ TheoryList.vo	List.vo 	SetoidList.vo  \
  ListTactics.vo )
 
 STRINGSVO:=$(addprefix theories/Strings/, \
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index c457a83c4..c6252de9c 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1325,7 +1325,7 @@ Proof.
  apply Hl; auto.
  constructor.
  apply Hr; eauto.
- apply (InA_InfA (PX.eqke_refl (elt:=elt))); intros (y',e') H6.
+ apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6.
  destruct (elements_aux_mapsto r acc y' e'); intuition.
  red; simpl; eauto.
  red; simpl; eauto.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 5565c048c..1d4bb8f11 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -571,7 +571,7 @@ Qed.
 (** First, [Equal] is [Equiv] with Leibniz on elements. *)
 
 Lemma Equal_Equiv : forall (m m' : t elt),
-  Equal m m' <-> Equiv (@Logic.eq elt) m m'.
+  Equal m m' <-> Equiv Logic.eq m m'.
 Proof.
 intros. rewrite Equal_mapsto_iff. split; intros.
 split.
@@ -760,6 +760,16 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Notation eqke := (@eq_key_elt elt).
   Notation eqk := (@eq_key elt).
 
+  Instance eqk_equiv : Equivalence eqk.
+  Proof. split; repeat red; eauto. Qed.
+
+  Instance eqke_equiv : Equivalence eqke.
+  Proof.
+   unfold eq_key_elt; split; repeat red; firstorder.
+   eauto with *.
+   congruence.
+  Qed.
+
   (** Complements about InA, NoDupA and findA *)
 
   Lemma InA_eqke_eqk : forall k1 k2 e1 e2 l,
@@ -787,12 +797,12 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   intros. symmetry.
   unfold eqb.
   rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
-   by eauto using NoDupA_rev; eauto.
+   by (eauto using NoDupA_rev with *); eauto.
   case_eq (findA (eqb k) (rev l)); auto.
   intros e.
   unfold eqb.
   rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
-   by eauto using NoDupA_rev.
+   by (eauto using NoDupA_rev with *).
   intro Eq; rewrite Eq; auto.
   Qed.
 
@@ -893,9 +903,9 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   assert (Hstep' : forall k e a m' m'', InA eqke (k,e) l -> ~In k m' ->
              Add k e m' m'' -> P m' a -> P m'' (F (k,e) a)).
    intros k e a m' m'' H ? ? ?; eapply Hstep; eauto.
-   revert H; unfold l; rewrite InA_rev, elements_mapsto_iff; auto.
+   revert H; unfold l; rewrite InA_rev, elements_mapsto_iff; auto with *.
   assert (Hdup : NoDupA eqk l).
-   unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto.
+   unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto with *.
    apply elements_3w.
   assert (Hsame : forall k, find k m = findA (eqb k) l).
    intros k. unfold l. rewrite elements_o, findA_rev; auto.
@@ -977,7 +987,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   set (l:=rev (elements m)).
   assert (Rstep' : forall k e a b, InA eqke (k,e) l ->
     R a b -> R (f k e a) (g k e b)) by
-    (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; auto).
+    (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; auto with *).
   clearbody l; clear Rstep m.
   induction l; simpl; auto.
   apply Rstep'; auto.
@@ -1087,66 +1097,49 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 ->
    eqA (fold f m1 i) (fold f m2 i).
   Proof.
-  assert (eqke_refl : forall p, eqke p p).
-   red; auto.
-  assert (eqke_sym : forall p p', eqke p p' -> eqke p' p).
-   intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition.
-  assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p'').
-   intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
-   intuition; eauto; congruence.
   intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
   apply fold_right_equivlistA_restr with
-    (R:=fun p p' => ~eqk p p') (eqA:=eqke) (eqB:=eqA); auto.
-  intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; simpl in *; apply Comp; auto.
-  unfold eq_key; auto.
-  intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl.
-   intuition eauto.
+    (R:=fun p p' => ~eqk p p') (eqA:=eqke) (eqB:=eqA); auto with *.
+  intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto.
+  unfold eq_key, eq_key_elt; repeat red. intuition eauto.
   intros (k,e) (k',e'); unfold eq_key; simpl; auto.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply ForallList2_equiv1 with (eqA:=eqk); try red ; unfold eq_key ; eauto.
-  apply NoDupA_rev; try red ; unfold eq_key; eauto. apply elements_3w.
+  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply ForallL2_equiv1 with (eqA:=eqk); try red ; unfold eq_key ; eauto with *.
+  apply NoDupA_rev; try red ; unfold eq_key; eauto with *. apply elements_3w.
   red; intros.
-  do 2 rewrite InA_rev.
-  destruct x; do 2 rewrite <- elements_mapsto_iff.
-  do 2 rewrite find_mapsto_iff.
-  rewrite H; split; auto.
+  rewrite 2 InA_rev by auto with *.
+  destruct x; rewrite <- 2 elements_mapsto_iff by auto with *.
+  rewrite 2 find_mapsto_iff by auto with *.
+  rewrite H. split; auto.
   Qed.
 
   Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 ->
    eqA (fold f m2 i) (f k e (fold f m1 i)).
   Proof.
-  assert (eqke_refl : forall p, eqke p p).
-   red; auto.
-  assert (eqke_sym : forall p p', eqke p p' -> eqke p' p).
-   intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition.
-  assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p'').
-   intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
-   intuition; eauto; congruence.
   intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
   set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
   change (f k e (fold_right f' i (rev (elements m1))))
    with (f' (k,e) (fold_right f' i (rev (elements m1)))).
   apply fold_right_add_restr with
-    (R:=fun p p'=>~eqk p p')(eqA:=eqke)(eqB:=eqA); auto.
-  intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *. apply Comp; auto.
+    (R:=fun p p'=>~eqk p p')(eqA:=eqke)(eqB:=eqA); auto with *.
+  intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. apply Comp; auto.
 
-  unfold eq_key; auto.
-  intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl.
-   intuition eauto.
+  unfold eq_key_elt, eq_key; repeat red; intuition eauto.
   unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply ForallList2_equiv1 with (eqA:=eqk); try red; unfold eq_key ; eauto.
-  apply NoDupA_rev; try red; eauto. apply elements_3w.
-  rewrite InA_rev.
+  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply ForallL2_equiv1 with (eqA:=eqk); try red; unfold eq_key ; eauto with *.
+  apply NoDupA_rev; try red; eauto with *. apply elements_3w.
+  rewrite InA_rev; auto with *.
   contradict H.
   exists e.
   rewrite elements_mapsto_iff; auto.
   intros a.
-  rewrite InA_cons; do 2 rewrite InA_rev;
-  destruct a as (a,b); do 2 rewrite <- elements_mapsto_iff.
-  do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl.
+  destruct a as (a,b).
+  rewrite InA_cons, 2 InA_rev, <- 2 elements_mapsto_iff,
+   2 find_mapsto_iff by (auto with *).
+  unfold eq_key_elt; simpl.
   rewrite H0.
   rewrite add_o.
   destruct (eq_dec k a); intuition.
@@ -1545,9 +1538,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   set (f:=fun (_:key)(_:elt)=>S).
   setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)).
   rewrite <- cardinal_fold.
-  intros. apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto.
-  apply Partition_fold with (eqA:=eq); try red; auto.
-  compute; auto.
+  apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto.
+  apply Partition_fold with (eqA:=eq); repeat red; auto.
   Qed.
 
   Lemma Partition_partition : forall m m1 m2, Partition m m1 m2 ->
@@ -1777,8 +1769,7 @@ Module OrdProperties (M:S).
   Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt),
    sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'.
   Proof.
-  apply SortA_equivlistA_eqlistA; eauto;
-  unfold O.eqke, O.ltk; simpl; intuition; eauto.
+  apply SortA_equivlistA_eqlistA; eauto with *.
   Qed.
 
   Ltac clean_eauto := unfold O.eqke, O.ltk; simpl; intuition; eauto.
@@ -1802,7 +1793,7 @@ Module OrdProperties (M:S).
    destruct (E.compare x y); intuition; try discriminate; ME.order.
   Qed.
 
-  Lemma gtb_compat : forall p, compat_bool eqke (gtb p).
+  Lemma gtb_compat : forall p, Proper (eqke==>eq) (gtb p).
   Proof.
    red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H.
    generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e''));
@@ -1817,7 +1808,7 @@ Module OrdProperties (M:S).
    rewrite <- H2; auto.
   Qed.
 
-  Lemma leb_compat : forall p, compat_bool eqke (leb p).
+  Lemma leb_compat : forall p, Proper (eqke==>eq) (leb p).
   Proof.
    red; intros x a b H.
    unfold leb; f_equal; apply gtb_compat; auto.
@@ -1829,7 +1820,7 @@ Module OrdProperties (M:S).
     elements m = elements_lt p m ++ elements_ge p m.
   Proof.
   unfold elements_lt, elements_ge, leb; intros.
-  apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with map.
+  apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with *.
   intros; destruct x; destruct y; destruct p.
   rewrite gtb_1 in H; unfold O.ltk in H; simpl in *.
   assert (~ltk (t1,e0) (k,e1)).
@@ -1843,14 +1834,14 @@ Module OrdProperties (M:S).
                  (elements_lt (x,e) m ++ (x,e):: elements_ge (x,e) m).
   Proof.
   intros; unfold elements_lt, elements_ge.
-  apply sort_equivlistA_eqlistA; auto with map.
-  apply (@SortA_app _ eqke); auto with map.
-  apply (@filter_sort _ eqke); auto with map; clean_eauto.
+  apply sort_equivlistA_eqlistA; auto with *.
+  apply (@SortA_app _ eqke); auto with *.
+  apply (@filter_sort _ eqke); auto with *; clean_eauto.
   constructor; auto with map.
-  apply (@filter_sort _ eqke); auto with map; clean_eauto.
-  rewrite (@InfA_alt _ eqke); auto with map; try (clean_eauto; fail).
+  apply (@filter_sort _ eqke); auto with *; clean_eauto.
+  rewrite (@InfA_alt _ eqke); auto with *; try (clean_eauto; fail).
   intros.
-  rewrite filter_InA in H1; auto with map; destruct H1.
+  rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite leb_1 in H2.
   destruct y; unfold O.ltk in *; simpl in *.
   rewrite <- elements_mapsto_iff in H1.
@@ -1858,24 +1849,22 @@ Module OrdProperties (M:S).
    contradict H.
    exists e0; apply MapsTo_1 with t0; auto.
   ME.order.
-  apply (@filter_sort _ eqke); auto with map; clean_eauto.
+  apply (@filter_sort _ eqke); auto with *; clean_eauto.
   intros.
-  rewrite filter_InA in H1; auto with map; destruct H1.
+  rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite gtb_1 in H3.
   destruct y; destruct x0; unfold O.ltk in *; simpl in *.
   inversion_clear H2.
   red in H4; simpl in *; destruct H4.
   ME.order.
-  rewrite filter_InA in H4; auto with map; destruct H4.
+  rewrite filter_InA in H4; auto with *; destruct H4.
   rewrite leb_1 in H4.
   unfold O.ltk in *; simpl in *; ME.order.
   red; intros a; destruct a.
-  rewrite InA_app_iff; rewrite InA_cons.
-  do 2 (rewrite filter_InA; auto with map).
-  do 2 rewrite <- elements_mapsto_iff.
-  rewrite leb_1; rewrite gtb_1.
-  rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
-  rewrite add_mapsto_iff.
+  rewrite InA_app_iff, InA_cons, 2 filter_InA,
+    <-2 elements_mapsto_iff, leb_1, gtb_1,
+    find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+    add_mapsto_iff by (auto with *).
   unfold O.eqke, O.ltk; simpl.
   destruct (E.compare t0 x); intuition.
   right; split; auto; ME.order.
@@ -1892,8 +1881,8 @@ Module OrdProperties (M:S).
      eqlistA eqke (elements m') (elements m ++ (x,e)::nil).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with map.
-  apply (@SortA_app _ eqke); auto with map.
+  apply sort_equivlistA_eqlistA; auto with *.
+  apply (@SortA_app _ eqke); auto with *.
   intros.
   inversion_clear H2.
   destruct x0; destruct y.
@@ -1903,11 +1892,10 @@ Module OrdProperties (M:S).
   apply H; firstorder.
   inversion H3.
   red; intros a; destruct a.
-  rewrite InA_app_iff; rewrite InA_cons; rewrite InA_nil.
-  do 2 rewrite <- elements_mapsto_iff.
-  rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
-  rewrite add_mapsto_iff; unfold O.eqke; simpl.
-  intuition.
+  rewrite InA_app_iff, InA_cons, InA_nil, <- 2 elements_mapsto_iff,
+   find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+   add_mapsto_iff by (auto with *).
+  unfold O.eqke; simpl. intuition.
   destruct (E.eq_dec x t0); auto.
   exfalso.
   assert (In t0 m).
@@ -1921,9 +1909,9 @@ Module OrdProperties (M:S).
      eqlistA eqke (elements m') ((x,e)::elements m).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with map.
+  apply sort_equivlistA_eqlistA; auto with *.
   change (sort ltk (((x,e)::nil) ++ elements m)).
-  apply (@SortA_app _ eqke); auto with map.
+  apply (@SortA_app _ eqke); auto with *.
   intros.
   inversion_clear H1.
   destruct y; destruct x0.
@@ -1933,11 +1921,10 @@ Module OrdProperties (M:S).
   apply H; firstorder.
   inversion H3.
   red; intros a; destruct a.
-  rewrite InA_cons.
-  do 2 rewrite <- elements_mapsto_iff.
-  rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
-  rewrite add_mapsto_iff; unfold O.eqke; simpl.
-  intuition.
+  rewrite InA_cons, <- 2 elements_mapsto_iff,
+    find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+    add_mapsto_iff by (auto with *).
+  unfold O.eqke; simpl. intuition.
   destruct (E.eq_dec x t0); auto.
   exfalso.
   assert (In t0 m).
@@ -1950,7 +1937,7 @@ Module OrdProperties (M:S).
    Equal m m' -> eqlistA eqke (elements m) (elements m').
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with map.
+  apply sort_equivlistA_eqlistA; auto with *.
   red; intros.
   destruct x; do 2 rewrite <- elements_mapsto_iff.
   do 2 rewrite find_mapsto_iff; rewrite H; split; auto.
@@ -2052,11 +2039,8 @@ Module OrdProperties (M:S).
   inversion_clear H1.
   red in H2; destruct H2; simpl in *; ME.order.
   inversion_clear H4.
-  rewrite (@InfA_alt _ eqke) in H3; eauto.
+  rewrite (@InfA_alt _ eqke) in H3; eauto with *.
   apply (H3 (y,x0)); auto.
-  unfold lt_key; simpl; intuition; eauto.
-  intros (x1,x2) (y1,y2) (z1,z2); compute; intuition; eauto.
-  intros (x1,x2) (y1,y2) (z1,z2); compute; intuition; eauto.
   Qed.
 
   Lemma min_elt_MapsTo :
@@ -2156,7 +2140,7 @@ Module OrdProperties (M:S).
   do 2 rewrite fold_1.
   do 2 rewrite <- fold_left_rev_right.
   apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
-  intros (k,e) (k',e') a a' (Hk,He) Ha; simpl in *; apply Hf; auto.
+  intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto.
   apply eqlistA_rev. apply elements_Equal_eqlistA. auto.
   Qed.
 
@@ -2169,7 +2153,7 @@ Module OrdProperties (M:S).
   set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
   transitivity (fold_right f' i (rev (elements m1 ++ (x,e)::nil))).
   apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
-  intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *. apply P; auto.
+  intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *. apply P; auto.
   apply eqlistA_rev.
   apply elements_Add_Above; auto.
   rewrite distr_rev; simpl.
@@ -2185,7 +2169,7 @@ Module OrdProperties (M:S).
   set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
   transitivity (fold_right f' i (rev (((x,e)::nil)++elements m1))).
   apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
-  intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *; apply P; auto.
+  intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *; apply P; auto.
   apply eqlistA_rev.
   simpl; apply elements_Add_Below; auto.
   rewrite distr_rev; simpl.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index da5b35874..f5ee8b23f 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -584,6 +584,10 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p').
 
+  Global Instance eqk_equiv : Equivalence eq_key.
+  Global Instance eqke_equiv : Equivalence eq_key_elt.
+  Global Instance ltk_strorder : StrictOrder lt_key.
+
   Lemma mem_find :
     forall m x, mem x m = match find x m with None => false | _ => true end.
   Proof.
@@ -764,8 +768,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   simpl; auto.
   destruct o; simpl; intros.
   (* Some *)
-  apply (SortA_app (eqA:=eq_key_elt)); auto.
-  compute; intuition.
+  apply (SortA_app (eqA:=eq_key_elt)); auto with *.
   constructor; auto.
   apply In_InfA; intros.
   destruct y0.
@@ -784,8 +787,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   eapply xelements_bits_lt_1; eauto.
   eapply xelements_bits_lt_2; eauto.
   (* None *)
-  apply (SortA_app (eqA:=eq_key_elt)); auto.
-  compute; intuition.
+  apply (SortA_app (eqA:=eq_key_elt)); auto with *.
   intros x0 y0.
   do 2 rewrite InA_alt.
   intros (y1,(Hy1,H)) (y2,(Hy2,H0)).
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 36964ad01..08071ec56 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1698,9 +1698,9 @@ Lemma L_eq_cons :
 Proof.
  unfold L.eq, L.Equal in |- *; intuition.
  inversion_clear H1; generalize (H0 a); clear H0; intuition.
- apply InA_eqA with x; eauto.
+ apply InA_eqA with x; eauto with *.
  inversion_clear H1; generalize (H0 a); clear H0; intuition.
- apply InA_eqA with y; eauto.
+ apply InA_eqA with y; eauto with *.
 Qed.
 Hint Resolve L_eq_cons.
 
@@ -2000,7 +2000,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  rewrite partition_in_2, filter_in; intuition.
  rewrite H2; auto.
  destruct (f a); auto.
- red; intros; f_equal.
+ repeat red; intros; f_equal.
  rewrite (H _ _ H0); auto.
  Qed.
 
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 796db9f8f..1b1bae352 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -133,7 +133,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
    forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}),
    compat_P E.eq P -> compat_bool E.eq (fdec Pdec).
   Proof.
-    unfold compat_P, compat_bool, fdec in |- *; intros.
+    unfold compat_P, compat_bool, Proper, respectful, fdec in |- *; intros.
     generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder.
   Qed.
 
@@ -217,7 +217,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
     intros s1 s2; simpl in |- *.
     intros; assert (compat_bool E.eq (fdec Pdec)); auto.
     intros; assert (compat_bool E.eq (fun x => negb (fdec Pdec x))).
-    generalize H2; unfold compat_bool in |- *; intuition;
+    generalize H2; unfold compat_bool, Proper, respectful in |- *; intuition;
      apply (f_equal negb); auto.
     intuition.
     generalize H4; unfold For_all, Equal in |- *; intuition.
@@ -662,7 +662,8 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
    forall f : elt -> bool,
    compat_bool E.eq f -> compat_P E.eq (fun x => f x = true).
   Proof.
-     unfold compat_bool, compat_P in |- *; intros; rewrite <- H1; firstorder.
+     unfold compat_bool, compat_P, Proper, respectful, impl; intros;
+      rewrite <- H1; firstorder.
   Qed.
 
   Hint Resolve compat_P_aux.
@@ -768,7 +769,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
     intro p; case p; clear p; intros s1 s2 H C.
     generalize (H (compat_P_aux C)); clear H; intro H.
     assert (D : compat_bool E.eq (fun x => negb (f x))).
-    generalize C; unfold compat_bool in |- *; intros; apply (f_equal negb);
+    generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb);
      auto.
     simpl in |- *; unfold Equal in |- *; intuition.
     apply filter_3; firstorder.
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index c95aa8025..ec0c6a559 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -592,11 +592,11 @@ Section Bool.
 (** Properties of [filter] *)
 
 Variable f:elt->bool.
-Variable Comp: compat_bool E.eq f.
+Variable Comp: Proper (E.eq==>Logic.eq) f.
 
-Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
+Let Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)).
 Proof.
-unfold compat_bool in *; intros; f_equal; auto.
+repeat red; intros; f_equal; auto.
 Qed.
 
 Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
@@ -695,7 +695,7 @@ Proof.
 clear Comp' Comp f.
 intros.
 assert (compat_bool E.eq (fun x => orb (f x) (g x))).
-  unfold compat_bool; intros.
+  unfold compat_bool, Proper, respectful; intros.
   rewrite (H x y H1);  rewrite (H0 x y H1); auto.
 unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto.
 assert (f a || g a = true <-> f a = true \/ g a = true).
@@ -785,7 +785,7 @@ Variable Comp: compat_bool E.eq f.
 
 Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
 Proof.
-unfold compat_bool in *; intros; f_equal; auto.
+unfold compat_bool, Proper, respectful in *; intros; f_equal; auto.
 Qed.
 
 Lemma exists_mem_1:
@@ -841,16 +841,16 @@ Notation compat_opL := (compat_op E.eq Logic.eq).
 Notation transposeL := (transpose Logic.eq).
 
 Lemma sum_plus :
-  forall f g, compat_nat E.eq f -> compat_nat E.eq g ->
+  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
     forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
 Proof.
 unfold sum.
 intros f g Hf Hg.
-assert (fc : compat_opL (fun x:elt =>plus (f x))).  auto.
+assert (fc : compat_opL (fun x:elt =>plus (f x))).  red; auto.
 assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
-assert (gc : compat_opL (fun x:elt => plus (g x))). auto.
+assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto.
 assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
-assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto.
+assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto.
 assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
 assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
 intros s;pattern s; apply set_rec.
@@ -869,8 +869,8 @@ Proof.
 unfold sum; intros f Hf.
 assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
 assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))).
- red; intros.
- rewrite (Hf x x' H); auto.
+ repeat red; intros.
+ rewrite (Hf _ _ H); auto.
 assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
  red; intros; omega.
 intros s;pattern s; apply set_rec.
@@ -912,17 +912,18 @@ transitivity (f x (fold f s0 i)).
 apply fold_add with (eqA:=eqA); auto with set.
 transitivity (g x (fold f s0 i)); auto with set.
 transitivity (g x (fold g s0 i)); auto with set.
+apply gc; auto with *.
 symmetry; apply fold_add with (eqA:=eqA); auto.
 do 2 rewrite fold_empty; reflexivity.
 Qed.
 
 Lemma sum_compat :
-  forall f g, compat_nat E.eq f -> compat_nat E.eq g ->
+  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
   forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
 intros.
-unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto.
-red; intros; omega.
-red; intros; omega.
+unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with *.
+intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
+intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
 Qed.
 
 End Sum.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 412b6f5c5..bd1472330 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -478,7 +478,7 @@ Lemma filter_ext : forall f f', compat_bool E.eq f -> (forall x, f x = f' x) ->
 Proof.
 intros f f' Hf Hff' s s' Hss' x. do 2 (rewrite filter_iff; auto).
 rewrite Hff', Hss'; intuition.
-red; intros; rewrite <- 2 Hff'; auto.
+repeat red; intros; rewrite <- 2 Hff'; auto.
 Qed.
 
 Lemma filter_subset : forall f, compat_bool E.eq f ->
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index bc2b7b64e..782dccae3 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -1067,7 +1067,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  rewrite partition_in_2, filter_in; intuition.
  rewrite H2; auto.
  destruct (f a); auto.
- red; intros; f_equal.
+ repeat red; intros; f_equal.
  rewrite (H _ _ H0); auto.
  Qed.
 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 032f0c1b3..84c26dacd 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -21,7 +21,7 @@ Require Import DecidableTypeEx FSetFacts FSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Hint Unfold transpose compat_op.
+Hint Unfold transpose compat_op Proper respectful.
 Hint Extern 1 (Equivalence _) => constructor; congruence.
 
 (** First, a functor for Weak Sets in functorial version. *)
@@ -358,9 +358,9 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' ->
            P s' a -> P s'' (f x a)).
    intros; eapply Pstep; eauto.
-   rewrite elements_iff, <- InA_rev; auto.
+   rewrite elements_iff, <- InA_rev; auto with *.
   assert (Hdup : NoDup l) by
-    (unfold l; eauto using elements_3w, NoDupA_rev).
+    (unfold l; eauto using elements_3w, NoDupA_rev with *).
   assert (Hsame : forall x, In x s <-> InA x l) by
     (unfold l; intros; rewrite elements_iff, InA_rev; intuition).
   clear Pstep; clearbody l; revert s Hsame; induction l.
@@ -429,7 +429,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   do 2 rewrite fold_1, <- fold_left_rev_right.
   set (l:=rev (elements s)).
   assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by
-    (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto).
+    (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto with *).
   clearbody l; clear Rstep s.
   induction l; simpl; auto.
   Qed.
@@ -481,8 +481,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
         fold f s i = fold_right f i l.
   Proof.
   intros; exists (rev (elements s)); split.
-  apply NoDupA_rev; auto with set.
-  exact E.eq_trans.
+  apply NoDupA_rev; auto with *.
   split; intros.
   rewrite elements_iff; do 2 rewrite InA_alt.
   split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
@@ -517,8 +516,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   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.
+  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto with *.
   rewrite <- Hl1; auto.
   intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1;
    rewrite (H2 a); intuition.
@@ -547,7 +545,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   intros.
   apply fold_rel with (R:=fun u v => eqA u (f x v)); intros.
   reflexivity.
-  transitivity (f x0 (f x b)); auto.
+  transitivity (f x0 (f x b)); auto. apply Comp; auto with *.
   Qed.
 
   (** ** Fold is a morphism *)
@@ -556,6 +554,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
    eqA (fold f s i) (fold f s i').
   Proof.
   intros. apply fold_rel with (R:=eqA); auto.
+   intros; apply Comp; auto with *.
   Qed.
 
   Lemma fold_equal :
@@ -910,7 +909,7 @@ Module OrdProperties (M:S).
   Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
    sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
   Proof.
-  apply SortA_equivlistA_eqlistA; eauto.
+  apply SortA_equivlistA_eqlistA; eauto with *.
   Qed.
 
   Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
@@ -929,7 +928,7 @@ Module OrdProperties (M:S).
    intros; unfold leb, gtb; destruct (E.compare x y); intuition; try discriminate; ME.order.
   Qed.
 
-  Lemma gtb_compat : forall x, compat_bool E.eq (gtb x).
+  Lemma gtb_compat : forall x, Proper (E.eq==>Logic.eq) (gtb x).
   Proof.
    red; intros x a b H.
    generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto.
@@ -943,7 +942,7 @@ Module OrdProperties (M:S).
    rewrite <- H1; auto.
   Qed.
 
-  Lemma leb_compat : forall x, compat_bool E.eq (leb x).
+  Lemma leb_compat : forall x, Proper (E.eq==>Logic.eq) (leb x).
   Proof.
    red; intros x a b H; unfold leb.
    f_equal; apply gtb_compat; auto.
@@ -954,8 +953,7 @@ Module OrdProperties (M:S).
    elements s = elements_lt x s ++ elements_ge x s.
   Proof.
   unfold elements_lt, elements_ge, leb; intros.
-  eapply (@filter_split _ E.eq); trivial with set; auto with set.
-   ME.order. ME.order. ME.order.
+  eapply (@filter_split _ E.eq _ E.lt); auto with *.
   intros.
   rewrite gtb_1 in H.
   assert (~E.lt y x).
@@ -969,34 +967,32 @@ Module OrdProperties (M:S).
   Proof.
   intros; unfold elements_ge, elements_lt.
   apply sort_equivlistA_eqlistA; auto with set.
-  apply (@SortA_app _ E.eq); auto.
-  apply (@filter_sort _ E.eq); auto with set; eauto with set.
+  apply (@SortA_app _ E.eq); auto with *.
+  apply (@filter_sort _ E.eq); auto with *.
   constructor; auto.
-  apply (@filter_sort _ E.eq); auto with set; eauto with set.
-  rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with set).
+  apply (@filter_sort _ E.eq); auto with *.
+  rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with *).
   intros.
-  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite leb_1 in H2.
   rewrite <- elements_iff in H1.
   assert (~E.eq x y).
    contradict H; rewrite H; auto.
   ME.order.
   intros.
-  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite gtb_1 in H3.
   inversion_clear H2.
   ME.order.
-  rewrite filter_InA in H4; auto; destruct H4.
+  rewrite filter_InA in H4; auto with *; destruct H4.
   rewrite leb_1 in H4.
   ME.order.
   red; intros a.
-  rewrite InA_app_iff; rewrite InA_cons.
-  do 2 (rewrite filter_InA; auto).
-  do 2 rewrite <- elements_iff.
-  rewrite leb_1; rewrite gtb_1.
-  rewrite (H0 a); intuition.
+  rewrite InA_app_iff, InA_cons, !filter_InA, <-elements_iff,
+   leb_1, gtb_1, (H0 a) by auto with *.
+  intuition.
   destruct (E.compare a x); intuition.
-  right; right; split; auto.
+  right; right; split; auto with *.
   ME.order.
   Qed.
 
@@ -1008,15 +1004,15 @@ Module OrdProperties (M:S).
      eqlistA E.eq (elements s') (elements s ++ x::nil).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with set.
-  apply (@SortA_app _ E.eq); auto with set.
+  apply sort_equivlistA_eqlistA; auto with *.
+  apply (@SortA_app _ E.eq); auto with *.
   intros.
   inversion_clear H2.
   rewrite <- elements_iff in H1.
   apply ME.lt_eq with x; auto.
   inversion H3.
   red; intros a.
-  rewrite InA_app_iff; rewrite InA_cons; rewrite InA_nil.
+  rewrite InA_app_iff, InA_cons, InA_nil by auto with *.
   do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
   Qed.
 
@@ -1025,9 +1021,9 @@ Module OrdProperties (M:S).
      eqlistA E.eq (elements s') (x::elements s).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with set.
+  apply sort_equivlistA_eqlistA; auto with *.
   change (sort E.lt ((x::nil) ++ elements s)).
-  apply (@SortA_app _ E.eq); auto with set.
+  apply (@SortA_app _ E.eq); auto with *.
   intros.
   inversion_clear H1.
   rewrite <- elements_iff in H2.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 20af2878b..8acb6a902 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -10,7 +10,7 @@
 
 Require Export List.
 Require Export Sorting.
-Require Export Setoid.
+Require Export Setoid Basics Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -32,27 +32,28 @@ Inductive InA (x : A) : list A -> Prop :=
 
 Hint Constructors InA.
 
+(** TODO: it would be nice to have a generic definition instead
+    of the previous one. Having [InA = ExistsL eqA] raises too
+    many compatibility issues. For now, we only state the equivalence: *)
+
+Lemma InA_altdef : forall x l, InA x l <-> ExistsL (eqA x) l.
+Proof. split; induction 1; auto. Qed.
+
 Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l.
 Proof.
- intuition.
- inversion H; auto.
+ intuition. invlist InA; auto.
 Qed.
 
 Lemma InA_nil : forall x, InA x nil <-> False.
 Proof.
- intuition.
- inversion H.
+ intuition. invlist InA.
 Qed.
 
 (** An alternative definition of [InA]. *)
 
 Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l.
 Proof.
- induction l; intuition.
- inversion H.
- firstorder.
- inversion H1; firstorder.
- firstorder; subst; auto.
+ intros; rewrite InA_altdef, ExistsL_exists; firstorder.
 Qed.
 
 (** A list without redundancy modulo the equality over [A]. *)
@@ -63,6 +64,9 @@ Inductive NoDupA : list A -> Prop :=
 
 Hint Constructors NoDupA.
 
+
+Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
+
 (** lists with same elements modulo [eqA] *)
 
 Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
@@ -76,39 +80,62 @@ Inductive eqlistA : list A -> list A -> Prop :=
 
 Hint Constructors eqlistA.
 
-(** Compatibility of a  boolean function with respect to an equality. *)
+(** Results concerning lists modulo [eqA] *)
 
-Definition compat_bool (f : A->bool) := forall x y, eqA x y -> f x = f y.
+Hypothesis eqA_equiv : Equivalence eqA.
 
-(** Compatibility of a function upon natural numbers. *)
+Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv).
+Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv).
+Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv).
 
-Definition compat_nat (f : A->nat) := forall x y, eqA x y -> f x = f y.
+(** First, the two notions [equivlistA] and [eqlistA] are indeed equivlances *)
 
-(** Compatibility of a predicate with respect to an equality. *)
+Global Instance equivlist_equiv : Equivalence equivlistA.
+Proof.
+ firstorder.
+Qed.
 
-Definition compat_P (P : A->Prop) := forall x y, eqA x y -> P x -> P y.
+Global Instance eqlistA_equiv : Equivalence eqlistA.
+Proof.
+ constructor; red.
+ induction x; auto.
+ induction 1; auto.
+ intros x y z H; revert z; induction H; auto.
+ inversion 1; subst; auto. invlist eqlistA; eauto with *.
+Qed.
 
-(** Results concerning lists modulo [eqA] *)
+(** Moreover, [eqlistA] implies [equivlistA]. A reverse result
+    will be proved later for sorted list without duplicates. *)
 
-Hypothesis eqA_refl : forall x, eqA x x.
-Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
-Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
+Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA.
+Proof.
+  intros x x' H. induction H.
+  intuition.
+  red; intros.
+  rewrite 2 InA_cons.
+  rewrite (IHeqlistA x0), H; intuition.
+Qed.
 
-Hint Resolve eqA_refl eqA_trans.
-Hint Immediate eqA_sym.
+(** InA is compatible with eqA (for its first arg) and with
+    equivlistA (and hence eqlistA) for its second arg *)
+
+Global Instance InA_compat : Proper (eqA==>equivlistA==>iff) InA.
+Proof.
+ intros x x' Hxx' l l' Hll'. rewrite (Hll' x).
+ rewrite 2 InA_alt; firstorder.
+Qed.
+
+(** For compatibility, an immediate consequence of [InA_compat] *)
 
 Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
 Proof.
- intros s x y.
- do 2 rewrite InA_alt.
- intros H (z,(U,V)).
- exists z; split; eauto.
+ intros l x y H H'. rewrite <- H; auto.
 Qed.
 Hint Immediate InA_eqA.
 
 Lemma In_InA : forall l x, In x l -> InA x l.
 Proof.
- simple induction l; simpl in |- *; intuition.
+ simple induction l; simpl; intuition.
  subst; auto.
 Qed.
 Hint Resolve In_InA.
@@ -117,7 +144,7 @@ Lemma InA_split : forall l x, InA x l ->
  exists l1, exists y, exists l2,
  eqA x y /\ l = l1++y::l2.
 Proof.
-induction l; inversion_clear 1.
+induction l; intros; inv.
 exists (@nil A); exists a; exists l; auto.
 destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))).
 exists (a::l1); exists y; exists l2; auto.
@@ -128,7 +155,7 @@ Lemma InA_app : forall l1 l2 x,
  InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
 Proof.
  induction l1; simpl in *; intuition.
- inversion_clear H; auto.
+ inv; auto.
  elim (IHl1 l2 x H0); auto.
 Qed.
 
@@ -153,107 +180,16 @@ Proof.
  rewrite <- In_rev; auto.
 Qed.
 
-(** Results concerning lists modulo [eqA] and [ltA] *)
 
-Variable ltA : A -> A -> Prop.
-
-Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z.
-Hypothesis ltA_not_eqA : forall x y, ltA x y -> ~ eqA x y.
-Hypothesis ltA_eqA : forall x y z, ltA x y -> eqA y z -> ltA x z.
-Hypothesis eqA_ltA : forall x y z, eqA x y -> ltA y z -> ltA x z.
-
-Hint Resolve ltA_trans.
-Hint Immediate ltA_eqA eqA_ltA.
-
-Notation InfA:=(lelistA ltA).
-Notation SortA:=(sort ltA).
-
-Hint Constructors lelistA sort.
-
-Lemma InfA_ltA :
- forall l x y, ltA x y -> InfA y l -> InfA x l.
-Proof.
- destruct l; constructor; inversion_clear H0;
- eapply ltA_trans; eauto.
-Qed.
-
-Lemma InfA_eqA :
- forall l x y, eqA x y -> InfA y l -> InfA x l.
-Proof.
- intro s; case s; constructor; inversion_clear H0; eauto.
-Qed.
-Hint Immediate InfA_ltA InfA_eqA.
-
-Lemma SortA_InfA_InA :
- forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
-Proof.
- simple induction l.
- intros; inversion H1.
- intros.
- inversion_clear H0; inversion_clear H1; inversion_clear H2.
- eapply ltA_eqA; eauto.
- eauto.
-Qed.
-
-Lemma In_InfA :
- forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
-Proof.
- simple induction l; simpl in |- *; intros; constructor; auto.
-Qed.
-
-Lemma InA_InfA :
- forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
-Proof.
- simple induction l; simpl in |- *; intros; constructor; auto.
-Qed.
-
-(* In fact, this may be used as an alternative definition for InfA: *)
-
-Lemma InfA_alt :
- forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
-Proof.
-split.
-intros; eapply SortA_InfA_InA; eauto.
-apply InA_InfA.
-Qed.
-
-Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
-Proof.
- induction l1; simpl; auto.
- inversion_clear 1; auto.
-Qed.
-
-Lemma SortA_app :
- forall l1 l2, SortA l1 -> SortA l2 ->
- (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
- SortA (l1 ++ l2).
-Proof.
- induction l1; simpl in *; intuition.
- inversion_clear H.
- constructor; auto.
- apply InfA_app; auto.
- destruct l2; auto.
-Qed.
 
 Section NoDupA.
 
-Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
-Proof.
- simple induction l; auto.
- intros x l' H H0.
- inversion_clear H0.
- constructor; auto.
- intro.
- assert (ltA x x) by (eapply SortA_InfA_InA; eauto).
- elim (ltA_not_eqA H3); auto.
-Qed.
-
 Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' ->
   (forall x, InA x l -> InA x l' -> False) ->
   NoDupA (l++l').
 Proof.
 induction l; simpl; auto; intros.
-inversion_clear H.
+inv.
 constructor.
 rewrite InA_alt; intros (y,(H4,H5)).
 destruct (in_app_or _ _ _ H5).
@@ -274,35 +210,36 @@ Proof.
 induction l.
 simpl; auto.
 simpl; intros.
-inversion_clear H.
+inv.
 apply NoDupA_app; auto.
 constructor; auto.
-intro H2; inversion H2.
+intro; inv.
 intros x.
 rewrite InA_alt.
 intros (x1,(H2,H3)).
-inversion_clear 1.
+intro; inv.
 destruct H0.
-apply InA_eqA with x1; eauto.
+rewrite <- H4, H2.
 apply In_InA.
 rewrite In_rev; auto.
-inversion H4.
 Qed.
 
 Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
 Proof.
- induction l; simpl in *; inversion_clear 1; auto.
+ induction l; simpl in *; intros; inv; auto.
  constructor; eauto.
  contradict H0.
- rewrite InA_app_iff in *; rewrite InA_cons; intuition.
+ rewrite InA_app_iff in *.
+ rewrite InA_cons.
+ intuition.
 Qed.
 
 Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l').
 Proof.
- induction l; simpl in *; inversion_clear 1; auto.
+ induction l; simpl in *; intros; inv; auto.
  constructor; eauto.
  assert (H2:=IHl _ _ H1).
- inversion_clear H2.
+ inv.
  rewrite InA_cons.
  red; destruct 1.
  apply H0.
@@ -314,233 +251,101 @@ Proof.
  eapply NoDupA_split; eauto.
 Qed.
 
-End NoDupA.
-
-(** Some results about [eqlistA] *)
-
-Section EqlistA.
-
-Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.
-Proof.
-induction 1; auto; simpl; congruence.
-Qed.
-
-Lemma eqlistA_app : forall l1 l1' l2 l2',
-   eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
-Proof.
-intros l1 l1' l2 l2' H; revert l2 l2'; induction H; simpl; auto.
-Qed.
-
-Lemma eqlistA_rev_app : forall l1 l1',
-   eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' ->
-   eqlistA ((rev l1)++l2) ((rev l1')++l2').
-Proof.
-induction 1; auto.
-simpl; intros.
-do 2 rewrite app_ass; simpl; auto.
-Qed.
-
-Lemma eqlistA_rev : forall l1 l1',
-   eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
-Proof.
-intros.
-rewrite (app_nil_end (rev l1)).
-rewrite (app_nil_end (rev l1')).
-apply eqlistA_rev_app; auto.
-Qed.
-
-Lemma SortA_equivlistA_eqlistA : forall l l',
-   SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
-Proof.
-induction l; destruct l'; simpl; intros; auto.
-destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.
-destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.
-inversion_clear H; inversion_clear H0.
-assert (forall y, InA y l -> ltA a y).
-intros; eapply SortA_InfA_InA with (l:=l); eauto.
-assert (forall y, InA y l' -> ltA a0 y).
-intros; eapply SortA_InfA_InA with (l:=l'); eauto.
-clear H3 H4.
-assert (eqA a a0).
- destruct (H1 a).
- destruct (H1 a0).
- assert (InA a (a0::l')) by auto.
- inversion_clear H8; auto.
- assert (InA a0 (a::l)) by auto.
- inversion_clear H8; auto.
- elim (@ltA_not_eqA a a); auto.
- apply ltA_trans with a0; auto.
-constructor; auto.
-apply IHl; auto.
-split; intros.
-destruct (H1 x).
-assert (H8 : InA x (a0::l')) by auto; inversion_clear H8; auto.
-elim (@ltA_not_eqA a x); eauto.
-destruct (H1 x).
-assert (H8 : InA x (a::l)) by auto; inversion_clear H8; auto.
-elim (@ltA_not_eqA a0 x); eauto.
-Qed.
-
-End EqlistA.
-
-(** A few things about [filter] *)
-
-Section Filter.
-
-Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
+Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y ->
+ NoDupA (x::l) -> NoDupA (l1++y::l2) ->
+ equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
 Proof.
-induction l; simpl; auto.
-inversion_clear 1; auto.
-destruct (f a); auto.
-constructor; auto.
-apply In_InfA; auto.
-intros.
-rewrite filter_In in H; destruct H.
-eapply SortA_InfA_InA; eauto.
+ intros; intro a.
+ generalize (H2 a).
+ rewrite !InA_app_iff, !InA_cons.
+ inv.
+ assert (SW:=NoDupA_swap H1). inv.
+ rewrite InA_app_iff in H0.
+ split; intros.
+ assert (~eqA a x) by (contradict H3; rewrite <- H3; auto).
+ assert (~eqA a y) by (rewrite <- H; auto).
+ tauto.
+ assert (OR : eqA a x \/ InA a l) by intuition. clear H6.
+ destruct OR as [EQN|INA]; auto.
+ elim H0.
+ rewrite <-H,<-EQN; auto.
 Qed.
 
-Lemma filter_InA : forall f, (compat_bool f) ->
- forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
-Proof.
-intros; do 2 rewrite InA_alt; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
-  rewrite (H _ _ H0); auto.
-destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
-  rewrite <- (H _ _ H0); auto.
-Qed.
+End NoDupA.
 
-Lemma filter_split :
- forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
- forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
-Proof.
-induction l; simpl; intros; auto.
-inversion_clear H0.
-pattern l at 1; rewrite IHl; auto.
-case_eq (f a); simpl; intros; auto.
-assert (forall e, In e l -> f e = false).
-  intros.
-  assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)).
-  case_eq (f e); simpl; intros; auto.
-  elim (@ltA_not_eqA e e); auto.
-  apply ltA_trans with a; eauto.
-replace (List.filter f l) with (@nil A); auto.
-generalize H3; clear; induction l; simpl; auto.
-case_eq (f a); auto; intros.
-rewrite H3 in H; auto; try discriminate.
-Qed.
 
-End Filter.
 
 Section Fold.
 
 Variable B:Type.
 Variable eqB:B->B->Prop.
-
-(** 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').
-
-(** Two-argument functions that allow to reorder their arguments. *)
-Definition transpose (f : A -> B -> B) :=
-  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
-
-(** A version of transpose with restriction on where it should hold *)
-Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
-  forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
-
 Variable st:Equivalence eqB.
 Variable f:A->B->B.
 Variable i:B.
-Variable Comp:compat_op f.
+Variable Comp:Proper (eqA==>eqB==>eqB) f.
 
 Lemma fold_right_eqlistA :
    forall s s', eqlistA s s' ->
    eqB (fold_right f i s) (fold_right f i s').
 Proof.
-induction 1; simpl; auto.
-reflexivity.
-Qed.
-
-Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y ->
- NoDupA (x::l) -> NoDupA (l1++y::l2) ->
- equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
-Proof.
- intros; intro a.
- generalize (H2 a).
- repeat rewrite InA_app_iff.
- do 2 rewrite InA_cons.
- inversion_clear H0.
- assert (SW:=NoDupA_swap H1).
- inversion_clear SW.
- rewrite InA_app_iff in H0.
- split; intros.
- assert (~eqA a x).
-  contradict H3; apply InA_eqA with a; auto.
- assert (~eqA a y).
-  contradict H8; eauto.
- intuition.
- assert (eqA a x \/ InA a l) by intuition.
- destruct H8; auto.
- elim H0.
- destruct H7; [left|right]; eapply InA_eqA; eauto.
+induction 1; simpl; auto with relations.
+apply Comp; auto.
 Qed.
 
-(** [ForallList2] : specifies that a certain binary predicate should
+(** [ForallL2] : specifies that a certain binary predicate should
     always hold when inspecting two different elements of the list. *)
 
-Inductive ForallList2 (R : A -> A -> Prop) : list A -> Prop :=
-  | ForallNil : ForallList2 R nil
+Inductive ForallL2 (R : A -> A -> Prop) : list A -> Prop :=
+  | ForallNil : ForallL2 R nil
   | ForallCons : forall a l,
      (forall b, In b l -> R a b) ->
-     ForallList2 R l -> ForallList2 R (a::l).
-Hint Constructors ForallList2.
+     ForallL2 R l -> ForallL2 R (a::l).
+Hint Constructors ForallL2.
 
-(** [NoDupA] can be written in terms of [ForallList2] *)
+(** [NoDupA] can be written in terms of [ForallL2] *)
 
-Lemma ForallList2_NoDupA : forall l,
- ForallList2 (fun a b => ~eqA a b) l <-> NoDupA l.
+Lemma ForallL2_NoDupA : forall l,
+ ForallL2 (fun a b => ~eqA a b) l <-> NoDupA l.
 Proof.
  induction l; split; intros; auto.
- inversion_clear H. constructor; [ | rewrite <- IHl; auto ].
+ invlist ForallL2. constructor; [ | rewrite <- IHl; auto ].
  rewrite InA_alt; intros (a',(Haa',Ha')).
  exact (H0 a' Ha' Haa').
- inversion_clear H. constructor; [ | rewrite IHl; auto ].
+ invlist NoDupA. constructor; [ | rewrite IHl; auto ].
  intros b Hb.
  contradict H0.
  rewrite InA_alt; exists b; auto.
 Qed.
 
-Lemma ForallList2_impl : forall (R R':A->A->Prop),
+Lemma ForallL2_impl : forall (R R':A->A->Prop),
  (forall a b, R a b -> R' a b) ->
- forall l, ForallList2 R l -> ForallList2 R' l.
+ forall l, ForallL2 R l -> ForallL2 R' l.
 Proof.
  induction 2; auto.
 Qed.
 
-(** The following definition is easier to use than [ForallList2]. *)
+(** The following definition is easier to use than [ForallL2]. *)
 
-Definition ForallList2_alt (R:A->A->Prop) l :=
+Definition ForallL2_alt (R:A->A->Prop) l :=
  forall a b, InA a l -> InA b l -> ~eqA a b -> R a b.
 
 Section Restriction.
 Variable R : A -> A -> Prop.
 
-(** [ForallList2] and [ForallList2_alt] are related, but no completely
+(** [ForallL2] and [ForallL2_alt] are related, but no completely
     equivalent. For proving one implication, we need to know that the
     list has no duplicated elements... *)
 
-Lemma ForallList2_equiv1 : forall l, NoDupA l ->
- ForallList2_alt R l -> ForallList2 R l.
+Lemma ForallL2_equiv1 : forall l, NoDupA l ->
+ ForallL2_alt R l -> ForallL2 R l.
 Proof.
  induction l; auto.
  constructor. intros b Hb.
- inversion_clear H.
+ inv.
  apply H0; auto.
- contradict H1.
- apply InA_eqA with b; auto.
+ contradict H1; rewrite H1; auto.
  apply IHl.
- inversion_clear H; auto.
+ inv; auto.
  intros b c Hb Hc Hneq.
  apply H0; auto.
 Qed.
@@ -548,53 +353,59 @@ Qed.
 (** ... and for proving the other implication, we need to be able
    to reverse and adapt relation [R] modulo [eqA]. *)
 
-Hypothesis R_sym : forall a b, R a b -> R b a.
-Hypothesis R_compat : forall a, compat_P (R a).
+Hypothesis R_sym : Symmetric R.
+Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.
 
-Lemma ForallList2_equiv2 : forall l,
- ForallList2 R l -> ForallList2_alt R l.
+Lemma ForallL2_equiv2 : forall l,
+ ForallL2 R l -> ForallL2_alt R l.
 Proof.
  induction l.
- intros _. red. intros a b Ha. inversion Ha.
+ intros _. red. intros a b Ha. inv.
  inversion_clear 1 as [|? ? H_R Hl].
  intros b c Hb Hc Hneq.
- inversion_clear Hb; inversion_clear Hc.
+ inv.
  (* b,c = a : impossible *)
  elim Hneq; eauto.
  (* b = a, c in l *)
  rewrite InA_alt in H0; destruct H0 as (d,(Hcd,Hd)).
- apply R_compat with d; auto.
- apply R_sym; apply R_compat with a; auto.
+ rewrite H, Hcd; auto.
  (* b in l, c = a *)
  rewrite InA_alt in H; destruct H as (d,(Hcd,Hd)).
- apply R_compat with a; auto.
- apply R_sym; apply R_compat with d; auto.
+ rewrite H0, Hcd; auto.
  (* b,c in l *)
  apply (IHl Hl); auto.
 Qed.
 
-Lemma ForallList2_equiv : forall l, NoDupA l ->
- (ForallList2 R l <-> ForallList2_alt R l).
+Lemma ForallL2_equiv : forall l, NoDupA l ->
+ (ForallL2 R l <-> ForallL2_alt R l).
 Proof.
-split; [apply ForallList2_equiv2|apply ForallList2_equiv1]; auto.
+split; [apply ForallL2_equiv2|apply ForallL2_equiv1]; auto.
 Qed.
 
-Lemma ForallList2_equivlistA : forall l l', NoDupA l' ->
- equivlistA l l' -> ForallList2 R l -> ForallList2 R l'.
+Lemma ForallL2_equivlistA : forall l l', NoDupA l' ->
+ equivlistA l l' -> ForallL2 R l -> ForallL2 R l'.
 Proof.
 intros.
-apply ForallList2_equiv1; auto.
+apply ForallL2_equiv1; auto.
 intros a b Ha Hb Hneq.
 red in H0; rewrite <- H0 in Ha,Hb.
 revert a b Ha Hb Hneq.
-change (ForallList2_alt R l).
-apply ForallList2_equiv2; auto.
+change (ForallL2_alt R l).
+apply ForallL2_equiv2; auto.
 Qed.
 
+(** Two-argument functions that allow to reorder their arguments. *)
+Definition transpose (f : A -> B -> B) :=
+  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
+
+(** A version of transpose with restriction on where it should hold *)
+Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
+  forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
+
 Variable TraR :transpose_restr R f.
 
 Lemma fold_right_commutes_restr :
-  forall s1 s2 x, ForallList2 R (s1++x::s2) ->
+  forall s1 s2 x, ForallL2 R (s1++x::s2) ->
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
 Proof.
 induction s1; simpl; auto; intros.
@@ -602,15 +413,15 @@ reflexivity.
 transitivity (f a (f x (fold_right f i (s1++s2)))).
 apply Comp; auto.
 apply IHs1.
-inversion_clear H; auto.
+invlist ForallL2; auto.
 apply TraR.
-inversion_clear H.
+invlist ForallL2; auto.
 apply H0.
 apply in_or_app; simpl; auto.
 Qed.
 
 Lemma fold_right_equivlistA_restr :
-  forall s s', NoDupA s -> NoDupA s' -> ForallList2 R s ->
+  forall s s', NoDupA s -> NoDupA s' -> ForallL2 R s ->
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
 Proof.
  simple induction s.
@@ -618,27 +429,26 @@ Proof.
  intros; reflexivity.
  unfold equivlistA; intros.
  destruct (H2 a).
- assert (X : InA a nil); auto; inversion X.
+ assert (InA a nil) by auto; inv.
  intros x l Hrec s' N N' F E; simpl in *.
- assert (InA x s').
-  rewrite <- (E x); auto.
+ assert (InA x s') by (rewrite <- (E x); auto).
  destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
  subst s'.
  transitivity (f x (fold_right f i (s1++s2))).
  apply Comp; auto.
  apply Hrec; auto.
- inversion_clear N; auto.
+ inv; auto.
  eapply NoDupA_split; eauto.
- inversion_clear F; auto.
+ invlist ForallL2; auto.
  eapply equivlistA_NoDupA_split; eauto.
  transitivity (f y (fold_right f i (s1++s2))).
  apply Comp; auto. reflexivity.
  symmetry; apply fold_right_commutes_restr.
- apply ForallList2_equivlistA with (x::l); auto.
+ apply ForallL2_equivlistA with (x::l); auto.
 Qed.
 
 Lemma fold_right_add_restr :
-  forall s' s x, NoDupA s -> NoDupA s' -> ForallList2 R s' -> ~ InA x s ->
+  forall s' s x, NoDupA s -> NoDupA s' -> ForallL2 R s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
 Proof.
  intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto.
@@ -656,6 +466,7 @@ Proof.
 induction s1; simpl; auto; intros.
 reflexivity.
 transitivity (f a (f x (fold_right f i (s1++s2)))); auto.
+apply Comp; auto.
 Qed.
 
 Lemma fold_right_equivlistA :
@@ -663,8 +474,8 @@ Lemma fold_right_equivlistA :
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
 Proof.
 intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True);
- try red; auto.
-apply ForallList2_equiv1; try red; auto.
+ repeat red; auto.
+apply ForallL2_equiv1; try red; auto.
 Qed.
 
 Lemma fold_right_add :
@@ -674,6 +485,8 @@ Proof.
  intros; apply (@fold_right_equivlistA s' (x::s)); auto.
 Qed.
 
+End Fold.
+
 Section Remove.
 
 Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
@@ -682,15 +495,15 @@ Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }.
 Proof.
 induction l.
 right; auto.
-red; inversion 1.
+intro; inv.
 destruct (eqA_dec x a).
 left; auto.
 destruct IHl.
 left; auto.
-right; red; inversion_clear 1; contradiction.
+right; intro; inv; contradiction.
 Qed.
 
-Fixpoint removeA (x : A) (l : list A){struct l} : list A :=
+Fixpoint removeA (x : A) (l : list A) : list A :=
   match l with
     | nil => nil
     | y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl)
@@ -708,21 +521,21 @@ Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
 Proof.
 induction l; simpl; auto.
 split.
-inversion_clear 1.
-destruct 1; inversion_clear H.
+intro; inv.
+destruct 1; inv.
 intros.
 destruct (eqA_dec x a); simpl; auto.
 rewrite IHl; split; destruct 1; split; auto.
-inversion_clear H; auto.
-destruct H0; apply eqA_trans with a; auto.
+inv; auto.
+destruct H0; transitivity a; auto.
 split.
-inversion_clear 1.
+intro; inv.
 split; auto.
 contradict n.
-apply eqA_trans with y; auto.
+transitivity y; auto.
 rewrite (IHl x y) in H0; destruct H0; auto.
-destruct 1; inversion_clear H; auto.
-constructor 2; rewrite IHl; auto.
+destruct 1; inv; auto.
+right; rewrite IHl; auto.
 Qed.
 
 Lemma removeA_NoDupA :
@@ -730,7 +543,7 @@ Lemma removeA_NoDupA :
 Proof.
 simple induction s; simpl; intros.
 auto.
-inversion_clear H0.
+inv.
 destruct (eqA_dec x a); simpl; auto.
 constructor; auto.
 rewrite removeA_InA.
@@ -748,24 +561,249 @@ contradict H.
 apply InA_eqA with x0; auto.
 rewrite <- (H0 x0) in H1.
 destruct H1.
-inversion_clear H1; auto.
+inv; auto.
 elim H2; auto.
 Qed.
 
 End Remove.
 
-End Fold.
 
+
+(** Results concerning lists modulo [eqA] and [ltA] *)
+
+Variable ltA : A -> A -> Prop.
+Hypothesis ltA_strorder : StrictOrder ltA.
+Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
+
+Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder).
+
+Notation InfA:=(lelistA ltA).
+Notation SortA:=(sort ltA).
+
+Hint Constructors lelistA sort.
+
+Lemma InfA_ltA :
+ forall l x y, ltA x y -> InfA y l -> InfA x l.
+Proof.
+ destruct l; constructor. inv; eauto.
+Qed.
+
+Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA.
+Proof.
+ intros x x' Hxx' l l' Hll'.
+ inversion_clear Hll'.
+ intuition.
+ split; intro; inv; constructor.
+ rewrite <- Hxx', <- H; auto.
+ rewrite Hxx', H; auto.
+Qed.
+
+(** For compatibility, can be deduced from [InfA_compat] *)
+Lemma InfA_eqA :
+ forall l x y, eqA x y -> InfA y l -> InfA x l.
+Proof.
+ intros l x y H; rewrite H; auto.
+Qed.
+Hint Immediate InfA_ltA InfA_eqA.
+
+Lemma SortA_InfA_InA :
+ forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
+Proof.
+ simple induction l.
+ intros. inv.
+ intros. inv.
+ setoid_replace x with a; auto.
+ eauto.
+Qed.
+
+Lemma In_InfA :
+ forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
+Proof.
+ simple induction l; simpl; intros; constructor; auto.
+Qed.
+
+Lemma InA_InfA :
+ forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
+Proof.
+ simple induction l; simpl; intros; constructor; auto.
+Qed.
+
+(* In fact, this may be used as an alternative definition for InfA: *)
+
+Lemma InfA_alt :
+ forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
+Proof.
+split.
+intros; eapply SortA_InfA_InA; eauto.
+apply InA_InfA.
+Qed.
+
+Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
+Proof.
+ induction l1; simpl; auto.
+ intros; inv; auto.
+Qed.
+
+Lemma SortA_app :
+ forall l1 l2, SortA l1 -> SortA l2 ->
+ (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
+ SortA (l1 ++ l2).
+Proof.
+ induction l1; simpl in *; intuition.
+ inv.
+ constructor; auto.
+ apply InfA_app; auto.
+ destruct l2; auto.
+Qed.
+
+Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
+Proof.
+ simple induction l; auto.
+ intros x l' H H0.
+ inv.
+ constructor; auto.
+ intro.
+ apply (StrictOrder_Irreflexive x).
+ eapply SortA_InfA_InA; eauto.
+Qed.
+
+
+(** Some results about [eqlistA] *)
+
+Section EqlistA.
+
+Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.
+Proof.
+induction 1; auto; simpl; congruence.
+Qed.
+
+Global Instance app_eqlistA_compat :
+ Proper (eqlistA==>eqlistA==>eqlistA) (@app A).
+Proof.
+ repeat red; induction 1; simpl; auto.
+Qed.
+
+(** For compatibility, can be deduced from app_eqlistA_compat **)
+Lemma eqlistA_app : forall l1 l1' l2 l2',
+   eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
+Proof.
+intros l1 l1' l2 l2' H H'; rewrite H, H'; reflexivity.
+Qed.
+
+Lemma eqlistA_rev_app : forall l1 l1',
+   eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' ->
+   eqlistA ((rev l1)++l2) ((rev l1')++l2').
+Proof.
+induction 1; auto.
+simpl; intros.
+do 2 rewrite app_ass; simpl; auto.
+Qed.
+
+Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A).
+Proof.
+repeat red. intros.
+rewrite (app_nil_end (rev x)), (app_nil_end (rev y)).
+apply eqlistA_rev_app; auto.
+Qed.
+
+Lemma eqlistA_rev : forall l1 l1',
+   eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
+Proof.
+apply rev_eqlistA_compat.
+Qed.
+
+Lemma SortA_equivlistA_eqlistA : forall l l',
+   SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
+Proof.
+induction l; destruct l'; simpl; intros; auto.
+destruct (H1 a); assert (InA a nil) by auto; inv.
+destruct (H1 a); assert (InA a nil) by auto; inv.
+inv.
+assert (forall y, InA y l -> ltA a y).
+intros; eapply SortA_InfA_InA with (l:=l); eauto.
+assert (forall y, InA y l' -> ltA a0 y).
+intros; eapply SortA_InfA_InA with (l:=l'); eauto.
+clear H3 H4.
+assert (eqA a a0).
+ destruct (H1 a).
+ destruct (H1 a0).
+ assert (InA a (a0::l')) by auto. inv; auto.
+ assert (InA a0 (a::l)) by auto. inv; auto.
+ elim (StrictOrder_Irreflexive a); eauto.
+constructor; auto.
+apply IHl; auto.
+split; intros.
+destruct (H1 x).
+assert (InA x (a0::l')) by auto. inv; auto.
+rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto.
+destruct (H1 x).
+assert (InA x (a::l)) by auto. inv; auto.
+rewrite H9,H3 in H4. elim (StrictOrder_Irreflexive a0); eauto.
+Qed.
+
+End EqlistA.
+
+(** A few things about [filter] *)
+
+Section Filter.
+
+Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
+Proof.
+induction l; simpl; auto.
+intros; inv; auto.
+destruct (f a); auto.
+constructor; auto.
+apply In_InfA; auto.
+intros.
+rewrite filter_In in H; destruct H.
+eapply SortA_InfA_InA; eauto.
+Qed.
+
+Implicit Arguments eq [ [A] ].
+
+Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
+ forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
+Proof.
+clear ltA ltA_compat ltA_strorder.
+intros; do 2 rewrite InA_alt; intuition.
+destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
+destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
+  rewrite (H _ _ H0); auto.
+destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
+  rewrite <- (H _ _ H0); auto.
+Qed.
+
+Lemma filter_split :
+ forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
+ forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
+Proof.
+induction l; simpl; intros; auto.
+inv.
+rewrite IHl at 1; auto.
+case_eq (f a); simpl; intros; auto.
+assert (forall e, In e l -> f e = false).
+  intros.
+  assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)).
+  case_eq (f e); simpl; intros; auto.
+  elim (StrictOrder_Irreflexive e).
+  transitivity a; auto.
+replace (List.filter f l) with (@nil A); auto.
+generalize H3; clear; induction l; simpl; auto.
+case_eq (f a); auto; intros.
+rewrite H3 in H; auto; try discriminate.
+Qed.
+
+End Filter.
 End Type_with_equality.
 
-Hint Unfold compat_bool compat_nat compat_P.
-Hint Constructors InA NoDupA sort lelistA eqlistA.
+
+Hint Constructors InA eqlistA NoDupA sort lelistA.
 
 Section Find.
+
 Variable A B : Type.
 Variable eqA : A -> A -> Prop.
-Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
-Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
+Hypothesis eqA_equiv : Equivalence eqA.
 Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
 
 Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B :=
@@ -780,32 +818,49 @@ Lemma findA_NoDupA :
  (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (a,b) l <->
   findA (fun a' => if eqA_dec a a' then true else false) l = Some b).
 Proof.
-induction l; simpl; intros.
+set (eqk := fun p p' : A*B => eqA (fst p) (fst p')).
+set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p').
+induction l; intros; simpl.
 split; intros; try discriminate.
-inversion H0.
+invlist InA.
 destruct a as (a',b'); rename a0 into a.
-inversion_clear H.
+invlist NoDupA.
 split; intros.
-inversion_clear H.
-simpl in *; destruct H2; subst b'.
+invlist InA.
+compute in H2; destruct H2. subst b'.
 destruct (eqA_dec a a'); intuition.
 destruct (eqA_dec a a'); simpl.
-destruct H0.
-generalize e H2 eqA_trans eqA_sym; clear.
+contradict H0.
+revert e H2; clear - eqA_equiv.
 induction l.
-inversion 2.
-inversion_clear 2; intros; auto.
+intros; invlist InA.
+intros; invlist InA; auto.
 destruct a0.
 compute in H; destruct H.
 subst b.
-constructor 1; auto.
-simpl.
-apply eqA_trans with a; auto.
+left; auto.
+compute.
+transitivity a; auto. symmetry; auto.
 rewrite <- IHl; auto.
 destruct (eqA_dec a a'); simpl in *.
-inversion H; clear H; intros; subst b'; auto.
-constructor 2.
-rewrite IHl; auto.
+left; split; simpl; congruence.
+right. rewrite IHl; auto.
 Qed.
 
 End Find.
+
+
+(** Compatibility aliases. [Proper] is rather to be used directly now.*)
+
+Definition compat_bool {A} (eqA:A->A->Prop)(f:A->bool) :=
+ Proper (eqA==>Logic.eq) f.
+
+Definition compat_nat {A} (eqA:A->A->Prop)(f:A->nat) :=
+ Proper (eqA==>Logic.eq) f.
+
+Definition compat_P {A} (eqA:A->A->Prop)(P:A->Prop) :=
+ Proper (eqA==>impl) P.
+
+Definition compat_op {A B} (eqA:A->A->Prop)(eqB:B->B->Prop)(f:A->B->B) :=
+ Proper (eqA==>eqB==>eqB) f.
+
diff --git a/theories/Lists/SetoidList2.v b/theories/Lists/SetoidList2.v
deleted file mode 100644
index 78226cb5d..000000000
--- a/theories/Lists/SetoidList2.v
+++ /dev/null
@@ -1,850 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Require Export List.
-Require Export Sorting.
-Require Export Setoid Basics Morphisms.
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(** * Logical relations over lists with respect to a setoid equality
-      or ordering. *)
-
-(** This can be seen as a complement of predicate [lelistA] and [sort]
-    found in [Sorting]. *)
-
-Section Type_with_equality.
-Variable A : Type.
-Variable eqA : A -> A -> Prop.
-
-(** Being in a list modulo an equality relation over type [A]. *)
-
-Inductive InA (x : A) : list A -> Prop :=
-  | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l)
-  | InA_cons_tl : forall y l, InA x l -> InA x (y :: l).
-
-Hint Constructors InA.
-
-(** TODO: it would be nice to have a generic definition instead
-    of the previous one. Having [InA = ExistsL eqA] raises too
-    many compatibility issues. For now, we only state the equivalence: *)
-
-Lemma InA_altdef : forall x l, InA x l <-> ExistsL (eqA x) l.
-Proof. split; induction 1; auto. Qed.
-
-Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l.
-Proof.
- intuition. invlist InA; auto.
-Qed.
-
-Lemma InA_nil : forall x, InA x nil <-> False.
-Proof.
- intuition. invlist InA.
-Qed.
-
-(** An alternative definition of [InA]. *)
-
-Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l.
-Proof.
- intros; rewrite InA_altdef, ExistsL_exists; firstorder.
-Qed.
-
-(** A list without redundancy modulo the equality over [A]. *)
-
-Inductive NoDupA : list A -> Prop :=
-  | NoDupA_nil : NoDupA nil
-  | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
-
-Hint Constructors NoDupA.
-
-
-Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
-
-(** lists with same elements modulo [eqA] *)
-
-Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
-
-(** lists with same elements modulo [eqA] at the same place *)
-
-Inductive eqlistA : list A -> list A -> Prop :=
-  | eqlistA_nil : eqlistA nil nil
-  | eqlistA_cons : forall x x' l l',
-      eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l').
-
-Hint Constructors eqlistA.
-
-(** Results concerning lists modulo [eqA] *)
-
-Hypothesis eqA_equiv : Equivalence eqA.
-
-Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv).
-Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv).
-Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv).
-
-(** First, the two notions [equivlistA] and [eqlistA] are indeed equivlances *)
-
-Global Instance equivlist_equiv : Equivalence equivlistA.
-Proof.
- firstorder.
-Qed.
-
-Global Instance eqlistA_equiv : Equivalence eqlistA.
-Proof.
- constructor; red.
- induction x; auto.
- induction 1; auto.
- intros x y z H; revert z; induction H; auto.
- inversion 1; subst; auto. invlist eqlistA; eauto with *.
-Qed.
-
-(** Moreover, [eqlistA] implies [equivlistA]. A reverse result
-    will be proved later for sorted list without duplicates. *)
-
-Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA.
-Proof.
-  intros x x' H. induction H.
-  intuition.
-  red; intros.
-  rewrite 2 InA_cons.
-  rewrite (IHeqlistA x0), H; intuition.
-Qed.
-
-(** InA is compatible with eqA (for its first arg) and with
-    equivlistA (and hence eqlistA) for its second arg *)
-
-Global Instance InA_compat : Proper (eqA==>equivlistA==>iff) InA.
-Proof.
- intros x x' Hxx' l l' Hll'. rewrite (Hll' x).
- rewrite 2 InA_alt; firstorder.
-Qed.
-
-(** For compatibility, an immediate consequence of [InA_compat] *)
-
-Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
-Proof.
- intros l x y H H'. rewrite <- H; auto.
-Qed.
-Hint Immediate InA_eqA.
-
-Lemma In_InA : forall l x, In x l -> InA x l.
-Proof.
- simple induction l; simpl; intuition.
- subst; auto.
-Qed.
-Hint Resolve In_InA.
-
-Lemma InA_split : forall l x, InA x l ->
- exists l1, exists y, exists l2,
- eqA x y /\ l = l1++y::l2.
-Proof.
-induction l; intros; inv.
-exists (@nil A); exists a; exists l; auto.
-destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))).
-exists (a::l1); exists y; exists l2; auto.
-split; simpl; f_equal; auto.
-Qed.
-
-Lemma InA_app : forall l1 l2 x,
- InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
-Proof.
- induction l1; simpl in *; intuition.
- inv; auto.
- elim (IHl1 l2 x H0); auto.
-Qed.
-
-Lemma InA_app_iff : forall l1 l2 x,
- InA x (l1 ++ l2) <-> InA x l1 \/ InA x l2.
-Proof.
- split.
- apply InA_app.
- destruct 1; generalize H; do 2 rewrite InA_alt.
- destruct 1 as (y,(H1,H2)); exists y; split; auto.
- apply in_or_app; auto.
- destruct 1 as (y,(H1,H2)); exists y; split; auto.
- apply in_or_app; auto.
-Qed.
-
-Lemma InA_rev : forall p m,
- InA p (rev m) <-> InA p m.
-Proof.
- intros; do 2 rewrite InA_alt.
- split; intros (y,H); exists y; intuition.
- rewrite In_rev; auto.
- rewrite <- In_rev; auto.
-Qed.
-
-
-
-Section NoDupA.
-
-Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' ->
-  (forall x, InA x l -> InA x l' -> False) ->
-  NoDupA (l++l').
-Proof.
-induction l; simpl; auto; intros.
-inv.
-constructor.
-rewrite InA_alt; intros (y,(H4,H5)).
-destruct (in_app_or _ _ _ H5).
-elim H2.
-rewrite InA_alt.
-exists y; auto.
-apply (H1 a).
-auto.
-rewrite InA_alt.
-exists y; auto.
-apply IHl; auto.
-intros.
-apply (H1 x); auto.
-Qed.
-
-Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
-Proof.
-induction l.
-simpl; auto.
-simpl; intros.
-inv.
-apply NoDupA_app; auto.
-constructor; auto.
-intro; inv.
-intros x.
-rewrite InA_alt.
-intros (x1,(H2,H3)).
-intro; inv.
-destruct H0.
-rewrite <- H4, H2.
-apply In_InA.
-rewrite In_rev; auto.
-Qed.
-
-Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
-Proof.
- induction l; simpl in *; intros; inv; auto.
- constructor; eauto.
- contradict H0.
- rewrite InA_app_iff in *.
- rewrite InA_cons.
- intuition.
-Qed.
-
-Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l').
-Proof.
- induction l; simpl in *; intros; inv; auto.
- constructor; eauto.
- assert (H2:=IHl _ _ H1).
- inv.
- rewrite InA_cons.
- red; destruct 1.
- apply H0.
- rewrite InA_app_iff in *; rewrite InA_cons; auto.
- apply H; auto.
- constructor.
- contradict H0.
- rewrite InA_app_iff in *; rewrite InA_cons; intuition.
- eapply NoDupA_split; eauto.
-Qed.
-
-Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y ->
- NoDupA (x::l) -> NoDupA (l1++y::l2) ->
- equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
-Proof.
- intros; intro a.
- generalize (H2 a).
- rewrite !InA_app_iff, !InA_cons.
- inv.
- assert (SW:=NoDupA_swap H1). inv.
- rewrite InA_app_iff in H0.
- split; intros.
- assert (~eqA a x) by (contradict H3; rewrite <- H3; auto).
- assert (~eqA a y) by (rewrite <- H; auto).
- tauto.
- assert (OR : eqA a x \/ InA a l) by intuition. clear H6.
- destruct OR as [EQN|INA]; auto.
- elim H0.
- rewrite <-H,<-EQN; auto.
-Qed.
-
-End NoDupA.
-
-
-
-Section Fold.
-
-Variable B:Type.
-Variable eqB:B->B->Prop.
-Variable st:Equivalence eqB.
-Variable f:A->B->B.
-Variable i:B.
-Variable Comp:Proper (eqA==>eqB==>eqB) f.
-
-Lemma fold_right_eqlistA :
-   forall s s', eqlistA s s' ->
-   eqB (fold_right f i s) (fold_right f i s').
-Proof.
-induction 1; simpl; auto with relations.
-apply Comp; auto.
-Qed.
-
-(** [ForallL2] : specifies that a certain binary predicate should
-    always hold when inspecting two different elements of the list. *)
-
-Inductive ForallL2 (R : A -> A -> Prop) : list A -> Prop :=
-  | ForallNil : ForallL2 R nil
-  | ForallCons : forall a l,
-     (forall b, In b l -> R a b) ->
-     ForallL2 R l -> ForallL2 R (a::l).
-Hint Constructors ForallL2.
-
-(** [NoDupA] can be written in terms of [ForallL2] *)
-
-Lemma ForallL2_NoDupA : forall l,
- ForallL2 (fun a b => ~eqA a b) l <-> NoDupA l.
-Proof.
- induction l; split; intros; auto.
- invlist ForallL2. constructor; [ | rewrite <- IHl; auto ].
- rewrite InA_alt; intros (a',(Haa',Ha')).
- exact (H0 a' Ha' Haa').
- invlist NoDupA. constructor; [ | rewrite IHl; auto ].
- intros b Hb.
- contradict H0.
- rewrite InA_alt; exists b; auto.
-Qed.
-
-Lemma ForallL2_impl : forall (R R':A->A->Prop),
- (forall a b, R a b -> R' a b) ->
- forall l, ForallL2 R l -> ForallL2 R' l.
-Proof.
- induction 2; auto.
-Qed.
-
-(** The following definition is easier to use than [ForallL2]. *)
-
-Definition ForallL2_alt (R:A->A->Prop) l :=
- forall a b, InA a l -> InA b l -> ~eqA a b -> R a b.
-
-Section Restriction.
-Variable R : A -> A -> Prop.
-
-(** [ForallL2] and [ForallL2_alt] are related, but no completely
-    equivalent. For proving one implication, we need to know that the
-    list has no duplicated elements... *)
-
-Lemma ForallL2_equiv1 : forall l, NoDupA l ->
- ForallL2_alt R l -> ForallL2 R l.
-Proof.
- induction l; auto.
- constructor. intros b Hb.
- inv.
- apply H0; auto.
- contradict H1; rewrite H1; auto.
- apply IHl.
- inv; auto.
- intros b c Hb Hc Hneq.
- apply H0; auto.
-Qed.
-
-(** ... and for proving the other implication, we need to be able
-   to reverse and adapt relation [R] modulo [eqA]. *)
-
-Hypothesis R_sym : Symmetric R.
-Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.
-
-Lemma ForallL2_equiv2 : forall l,
- ForallL2 R l -> ForallL2_alt R l.
-Proof.
- induction l.
- intros _. red. intros a b Ha. inv.
- inversion_clear 1 as [|? ? H_R Hl].
- intros b c Hb Hc Hneq.
- inv.
- (* b,c = a : impossible *)
- elim Hneq; eauto.
- (* b = a, c in l *)
- rewrite InA_alt in H0; destruct H0 as (d,(Hcd,Hd)).
- rewrite H, Hcd; auto.
- (* b in l, c = a *)
- rewrite InA_alt in H; destruct H as (d,(Hcd,Hd)).
- rewrite H0, Hcd; auto.
- (* b,c in l *)
- apply (IHl Hl); auto.
-Qed.
-
-Lemma ForallL2_equiv : forall l, NoDupA l ->
- (ForallL2 R l <-> ForallL2_alt R l).
-Proof.
-split; [apply ForallL2_equiv2|apply ForallL2_equiv1]; auto.
-Qed.
-
-Lemma ForallL2_equivlistA : forall l l', NoDupA l' ->
- equivlistA l l' -> ForallL2 R l -> ForallL2 R l'.
-Proof.
-intros.
-apply ForallL2_equiv1; auto.
-intros a b Ha Hb Hneq.
-red in H0; rewrite <- H0 in Ha,Hb.
-revert a b Ha Hb Hneq.
-change (ForallL2_alt R l).
-apply ForallL2_equiv2; auto.
-Qed.
-
-(** Two-argument functions that allow to reorder their arguments. *)
-Definition transpose (f : A -> B -> B) :=
-  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
-
-(** A version of transpose with restriction on where it should hold *)
-Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
-  forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
-
-Variable TraR :transpose_restr R f.
-
-Lemma fold_right_commutes_restr :
-  forall s1 s2 x, ForallL2 R (s1++x::s2) ->
-  eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
-Proof.
-induction s1; simpl; auto; intros.
-reflexivity.
-transitivity (f a (f x (fold_right f i (s1++s2)))).
-apply Comp; auto.
-apply IHs1.
-invlist ForallL2; auto.
-apply TraR.
-invlist ForallL2; auto.
-apply H0.
-apply in_or_app; simpl; auto.
-Qed.
-
-Lemma fold_right_equivlistA_restr :
-  forall s s', NoDupA s -> NoDupA s' -> ForallL2 R s ->
-  equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
-Proof.
- simple induction s.
- destruct s'; simpl.
- intros; reflexivity.
- unfold equivlistA; intros.
- destruct (H2 a).
- assert (InA a nil) by auto; inv.
- intros x l Hrec s' N N' F E; simpl in *.
- assert (InA x s') by (rewrite <- (E x); auto).
- destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
- subst s'.
- transitivity (f x (fold_right f i (s1++s2))).
- apply Comp; auto.
- apply Hrec; auto.
- inv; auto.
- eapply NoDupA_split; eauto.
- invlist ForallL2; auto.
- eapply equivlistA_NoDupA_split; eauto.
- transitivity (f y (fold_right f i (s1++s2))).
- apply Comp; auto. reflexivity.
- symmetry; apply fold_right_commutes_restr.
- apply ForallL2_equivlistA with (x::l); auto.
-Qed.
-
-Lemma fold_right_add_restr :
-  forall s' s x, NoDupA s -> NoDupA s' -> ForallL2 R s' -> ~ InA x s ->
-  equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
-Proof.
- intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto.
-Qed.
-
-End Restriction.
-
-(** we now state similar results, but without restriction on transpose. *)
-
-Variable Tra :transpose f.
-
-Lemma fold_right_commutes : forall s1 s2 x,
-  eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
-Proof.
-induction s1; simpl; auto; intros.
-reflexivity.
-transitivity (f a (f x (fold_right f i (s1++s2)))); auto.
-apply Comp; auto.
-Qed.
-
-Lemma fold_right_equivlistA :
-  forall s s', NoDupA s -> NoDupA s' ->
-  equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
-Proof.
-intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True);
- repeat red; auto.
-apply ForallL2_equiv1; try red; auto.
-Qed.
-
-Lemma fold_right_add :
-  forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
-  equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
-Proof.
- intros; apply (@fold_right_equivlistA s' (x::s)); auto.
-Qed.
-
-End Fold.
-
-Section Remove.
-
-Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
-
-Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }.
-Proof.
-induction l.
-right; auto.
-intro; inv.
-destruct (eqA_dec x a).
-left; auto.
-destruct IHl.
-left; auto.
-right; intro; inv; contradiction.
-Qed.
-
-Fixpoint removeA (x : A) (l : list A) : list A :=
-  match l with
-    | nil => nil
-    | y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl)
-  end.
-
-Lemma removeA_filter : forall x l,
-  removeA x l = filter (fun y => if eqA_dec x y then false else true) l.
-Proof.
-induction l; simpl; auto.
-destruct (eqA_dec x a); auto.
-rewrite IHl; auto.
-Qed.
-
-Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
-Proof.
-induction l; simpl; auto.
-split.
-intro; inv.
-destruct 1; inv.
-intros.
-destruct (eqA_dec x a); simpl; auto.
-rewrite IHl; split; destruct 1; split; auto.
-inv; auto.
-destruct H0; transitivity a; auto.
-split.
-intro; inv.
-split; auto.
-contradict n.
-transitivity y; auto.
-rewrite (IHl x y) in H0; destruct H0; auto.
-destruct 1; inv; auto.
-right; rewrite IHl; auto.
-Qed.
-
-Lemma removeA_NoDupA :
-  forall s x, NoDupA s ->  NoDupA (removeA x s).
-Proof.
-simple induction s; simpl; intros.
-auto.
-inv.
-destruct (eqA_dec x a); simpl; auto.
-constructor; auto.
-rewrite removeA_InA.
-intuition.
-Qed.
-
-Lemma removeA_equivlistA : forall l l' x,
-  ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
-Proof.
-unfold equivlistA; intros.
-rewrite removeA_InA.
-split; intros.
-rewrite <- H0; split; auto.
-contradict H.
-apply InA_eqA with x0; auto.
-rewrite <- (H0 x0) in H1.
-destruct H1.
-inv; auto.
-elim H2; auto.
-Qed.
-
-End Remove.
-
-
-
-(** Results concerning lists modulo [eqA] and [ltA] *)
-
-Variable ltA : A -> A -> Prop.
-Hypothesis ltA_strorder : StrictOrder ltA.
-Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
-
-Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder).
-
-Notation InfA:=(lelistA ltA).
-Notation SortA:=(sort ltA).
-
-Hint Constructors lelistA sort.
-
-Lemma InfA_ltA :
- forall l x y, ltA x y -> InfA y l -> InfA x l.
-Proof.
- destruct l; constructor. inv; eauto.
-Qed.
-
-Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA.
-Proof.
- intros x x' Hxx' l l' Hll'.
- inversion_clear Hll'.
- intuition.
- split; intro; inv; constructor.
- rewrite <- Hxx', <- H; auto.
- rewrite Hxx', H; auto.
-Qed.
-
-(** For compatibility, can be deduced from [InfA_compat] *)
-Lemma InfA_eqA :
- forall l x y, eqA x y -> InfA y l -> InfA x l.
-Proof.
- intros l x y H; rewrite H; auto.
-Qed.
-Hint Immediate InfA_ltA InfA_eqA.
-
-Lemma SortA_InfA_InA :
- forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
-Proof.
- simple induction l.
- intros. inv.
- intros. inv.
- setoid_replace x with a; auto.
- eauto.
-Qed.
-
-Lemma In_InfA :
- forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
-Proof.
- simple induction l; simpl; intros; constructor; auto.
-Qed.
-
-Lemma InA_InfA :
- forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
-Proof.
- simple induction l; simpl; intros; constructor; auto.
-Qed.
-
-(* In fact, this may be used as an alternative definition for InfA: *)
-
-Lemma InfA_alt :
- forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
-Proof.
-split.
-intros; eapply SortA_InfA_InA; eauto.
-apply InA_InfA.
-Qed.
-
-Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
-Proof.
- induction l1; simpl; auto.
- intros; inv; auto.
-Qed.
-
-Lemma SortA_app :
- forall l1 l2, SortA l1 -> SortA l2 ->
- (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
- SortA (l1 ++ l2).
-Proof.
- induction l1; simpl in *; intuition.
- inv.
- constructor; auto.
- apply InfA_app; auto.
- destruct l2; auto.
-Qed.
-
-Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
-Proof.
- simple induction l; auto.
- intros x l' H H0.
- inv.
- constructor; auto.
- intro.
- apply (StrictOrder_Irreflexive x).
- eapply SortA_InfA_InA; eauto.
-Qed.
-
-
-(** Some results about [eqlistA] *)
-
-Section EqlistA.
-
-Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.
-Proof.
-induction 1; auto; simpl; congruence.
-Qed.
-
-Global Instance app_eqlistA_compat :
- Proper (eqlistA==>eqlistA==>eqlistA) (@app A).
-Proof.
- repeat red; induction 1; simpl; auto.
-Qed.
-
-(** For compatibility, can be deduced from app_eqlistA_compat **)
-Lemma eqlistA_app : forall l1 l1' l2 l2',
-   eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
-Proof.
-intros l1 l1' l2 l2' H H'; rewrite H, H'; reflexivity.
-Qed.
-
-Lemma eqlistA_rev_app : forall l1 l1',
-   eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' ->
-   eqlistA ((rev l1)++l2) ((rev l1')++l2').
-Proof.
-induction 1; auto.
-simpl; intros.
-do 2 rewrite app_ass; simpl; auto.
-Qed.
-
-Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A).
-Proof.
-repeat red. intros.
-rewrite (app_nil_end (rev x)), (app_nil_end (rev y)).
-apply eqlistA_rev_app; auto.
-Qed.
-
-Lemma eqlistA_rev : forall l1 l1',
-   eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
-Proof.
-apply rev_eqlistA_compat.
-Qed.
-
-Lemma SortA_equivlistA_eqlistA : forall l l',
-   SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
-Proof.
-induction l; destruct l'; simpl; intros; auto.
-destruct (H1 a); assert (InA a nil) by auto; inv.
-destruct (H1 a); assert (InA a nil) by auto; inv.
-inv.
-assert (forall y, InA y l -> ltA a y).
-intros; eapply SortA_InfA_InA with (l:=l); eauto.
-assert (forall y, InA y l' -> ltA a0 y).
-intros; eapply SortA_InfA_InA with (l:=l'); eauto.
-clear H3 H4.
-assert (eqA a a0).
- destruct (H1 a).
- destruct (H1 a0).
- assert (InA a (a0::l')) by auto. inv; auto.
- assert (InA a0 (a::l)) by auto. inv; auto.
- elim (StrictOrder_Irreflexive a); eauto.
-constructor; auto.
-apply IHl; auto.
-split; intros.
-destruct (H1 x).
-assert (InA x (a0::l')) by auto. inv; auto.
-rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto.
-destruct (H1 x).
-assert (InA x (a::l)) by auto. inv; auto.
-rewrite H9,H3 in H4. elim (StrictOrder_Irreflexive a0); eauto.
-Qed.
-
-End EqlistA.
-
-(** A few things about [filter] *)
-
-Section Filter.
-
-Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
-Proof.
-induction l; simpl; auto.
-intros; inv; auto.
-destruct (f a); auto.
-constructor; auto.
-apply In_InfA; auto.
-intros.
-rewrite filter_In in H; destruct H.
-eapply SortA_InfA_InA; eauto.
-Qed.
-
-Implicit Arguments eq [ [A] ].
-
-Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
- forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
-Proof.
-clear ltA ltA_compat ltA_strorder.
-intros; do 2 rewrite InA_alt; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
-  rewrite (H _ _ H0); auto.
-destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
-  rewrite <- (H _ _ H0); auto.
-Qed.
-
-Lemma filter_split :
- forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
- forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
-Proof.
-induction l; simpl; intros; auto.
-inv.
-rewrite IHl at 1; auto.
-case_eq (f a); simpl; intros; auto.
-assert (forall e, In e l -> f e = false).
-  intros.
-  assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)).
-  case_eq (f e); simpl; intros; auto.
-  elim (StrictOrder_Irreflexive e).
-  transitivity a; auto.
-replace (List.filter f l) with (@nil A); auto.
-generalize H3; clear; induction l; simpl; auto.
-case_eq (f a); auto; intros.
-rewrite H3 in H; auto; try discriminate.
-Qed.
-
-End Filter.
-End Type_with_equality.
-
-
-Hint Constructors InA eqlistA NoDupA sort lelistA.
-
-Section Find.
-
-Variable A B : Type.
-Variable eqA : A -> A -> Prop.
-Hypothesis eqA_equiv : Equivalence eqA.
-Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
-
-Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B :=
- match l with
-  | nil => None
-  | (a,b)::l => if f a then Some b else findA f l
- end.
-
-Lemma findA_NoDupA :
- forall l a b,
- NoDupA (fun p p' => eqA (fst p) (fst p')) l ->
- (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (a,b) l <->
-  findA (fun a' => if eqA_dec a a' then true else false) l = Some b).
-Proof.
-set (eqk := fun p p' : A*B => eqA (fst p) (fst p')).
-set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p').
-induction l; intros; simpl.
-split; intros; try discriminate.
-invlist InA.
-destruct a as (a',b'); rename a0 into a.
-invlist NoDupA.
-split; intros.
-invlist InA.
-compute in H2; destruct H2. subst b'.
-destruct (eqA_dec a a'); intuition.
-destruct (eqA_dec a a'); simpl.
-contradict H0.
-revert e H2; clear - eqA_equiv.
-induction l.
-intros; invlist InA.
-intros; invlist InA; auto.
-destruct a0.
-compute in H; destruct H.
-subst b.
-left; auto.
-compute.
-transitivity a; auto. symmetry; auto.
-rewrite <- IHl; auto.
-destruct (eqA_dec a a'); simpl in *.
-left; split; simpl; congruence.
-right. rewrite IHl; auto.
-Qed.
-
-End Find.
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 803a6143f..1f1ecddcd 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -20,18 +20,73 @@ Section Perm.
 
 Variable A : Type.
 Variable eqA : relation A.
+Hypothesis eqA_equiv : Equivalence eqA.
 Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
 Notation permutation := (permutation _ eqA_dec).
 Notation list_contents := (list_contents _ eqA_dec).
 
-(** The following lemmas need some knowledge on [eqA] *)
+(** we can use [multiplicity] to define [InA] and [NoDupA]. *)
 
-Variable eqA_refl : forall x, eqA x x.
-Variable eqA_sym : forall x y, eqA x y -> eqA y x.
-Variable eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
+Fact if_eqA_then : forall a a' (B:Type)(b b':B),
+ eqA a a' -> (if eqA_dec a a' then b else b') = b.
+Proof.
+  intros. destruct eqA_dec as [_|NEQ]; auto.
+  contradict NEQ; auto.
+Qed.
 
-(** we can use [multiplicity] to define [InA] and [NoDupA]. *)
+Fact if_eqA_else : forall a a' (B:Type)(b b':B),
+ ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.
+Proof.
+  intros. decide (eqA_dec a a') with H; auto.
+Qed.
+
+Fact if_eqA_refl : forall a (B:Type)(b b':B),
+ (if eqA_dec a a then b else b') = b.
+Proof.
+  intros; apply (decide_left (eqA_dec a a)); auto with *.
+Qed.
+
+(** PL: Inutilisable dans un rewrite sans un change prealable. *)
+
+Global Instance if_eqA (B:Type)(b b':B) :
+ Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').
+Proof.
+ intros B b b' x x' Hxx' y y' Hyy'.
+ intros; destruct (eqA_dec x y) as [H|H];
+  destruct (eqA_dec x' y') as [H'|H']; auto.
+ contradict H'; transitivity x; auto with *; transitivity y; auto with *.
+ contradict H; transitivity x'; auto with *; transitivity y'; auto with *.
+Qed.
+
+Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
+ eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
+               (if eqA_dec a1' a2 then b else b').
+Proof.
+ intros; destruct (eqA_dec a1 a2) as [A1|A1];
+  destruct (eqA_dec a1' a2) as [A1'|A1']; auto.
+ contradict A1'; transitivity a1; eauto with *.
+ contradict A1; transitivity a1'; eauto with *.
+Qed.
+
+Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
+ eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
+               (if eqA_dec a1 a2' then b else b').
+Proof.
+ intros; destruct (eqA_dec a1 a2) as [A2|A2];
+  destruct (eqA_dec a1 a2') as [A2'|A2']; auto.
+ contradict A2'; transitivity a2; eauto with *.
+ contradict A2; transitivity a2'; eauto with *.
+Qed.
+
+
+Global Instance multiplicity_eqA (l:list A) :
+ Proper (eqA==>@eq _) (multiplicity (list_contents l)).
+Proof.
+  intros l x x' Hxx'.
+  induction l as [|y l Hl]; simpl; auto.
+  rewrite (@if_eqA_rewrite_r y x x'); auto.
+Qed.
 
 Lemma multiplicity_InA :
   forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
@@ -40,15 +95,10 @@ Proof.
   simpl.
   split; inversion 1.
   simpl.
-  split; intros.
-  inversion_clear H.
-  destruct (eqA_dec a a0) as [_|H1]; auto with arith.
-  destruct H1; auto.
-  destruct (eqA_dec a a0); auto with arith.
-  simpl; rewrite <- IHl; auto.
-  destruct (eqA_dec a a0) as [H0|H0]; auto.
-  simpl in H.
-  constructor 2; rewrite IHl; auto.
+  intros a'; split; intros H. inversion_clear H.
+  apply (decide_left (eqA_dec a a')); auto with *.
+  destruct (eqA_dec a a'); auto with *. simpl; rewrite <- IHl; auto.
+  destruct (eqA_dec a a'); auto with *. right. rewrite IHl; auto.
 Qed.
 
 Lemma multiplicity_InA_O :
@@ -74,21 +124,17 @@ Proof.
   split; simpl.
   inversion_clear 1.
   rewrite IHl in H1.
-  intros; destruct (eqA_dec a a0) as [H2|H2]; simpl; auto.
+  intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *.
+  rewrite <- EQ.
   rewrite multiplicity_InA_O; auto.
-  contradict H0.
-  apply InA_eqA with a0; auto.
   intros; constructor.
   rewrite multiplicity_InA.
-  generalize (H a).
-  destruct (eqA_dec a a) as [H0|H0].
-  destruct (multiplicity (list_contents l) a); auto with arith.
-  simpl; inversion 1.
-  inversion H3.
-  destruct H0; auto.
+  specialize (H a).
+  rewrite if_eqA_refl in H.
+  clear IHl; omega.
   rewrite IHl; intros.
-  generalize (H a0); auto with arith.
-  destruct (eqA_dec a a0); simpl; auto with arith.
+  specialize (H a0); auto with *.
+  destruct (eqA_dec a a0); simpl; auto with *.
 Qed.
 
 
@@ -105,7 +151,7 @@ Qed.
 Lemma permut_cons_InA :
   forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
 Proof.
-  intros; apply (permut_InA_InA (e:=e) H); auto.
+  intros; apply (permut_InA_InA (e:=e) H); auto with *.
 Qed.
 
 (** Permutation of an empty list. *)
@@ -113,7 +159,7 @@ Lemma permut_nil :
   forall l, permutation l nil -> l = nil.
 Proof.
   intro l; destruct l as [ | e l ]; trivial.
-  assert (InA eqA e (e::l)) by auto.
+  assert (InA eqA e (e::l)) by (auto with *).
   intro Abs; generalize (permut_InA_InA Abs H).
   inversion 1.
 Qed.
@@ -123,10 +169,10 @@ Qed.
 Lemma permut_length_1:
   forall a b, permutation (a :: nil) (b :: nil)  -> eqA a b.
 Proof.
-  intros a b; unfold Permutation.permutation, meq; intro P;
-  generalize (P b); clear P; simpl.
-  destruct (eqA_dec b b) as [H|H]; [ | destruct H; auto].
-  destruct (eqA_dec a b); simpl; auto; intros; discriminate.
+  intros a b; unfold Permutation.permutation, meq.
+  intro P; specialize (P b); simpl in *.
+  rewrite if_eqA_refl in *.
+  destruct (eqA_dec a b); simpl; auto; discriminate.
 Qed.
 
 Lemma permut_length_2 :
@@ -139,22 +185,19 @@ Proof.
   left; split; auto.
   apply permut_length_1.
   red; red; intros.
-  generalize (P a); clear P; simpl.
-  destruct (eqA_dec a1 a) as [H2|H2];
-    destruct (eqA_dec a2 a) as [H3|H3]; auto.
-  destruct H3; apply eqA_trans with a1; auto.
-  destruct H2; apply eqA_trans with a2; auto.
+  specialize (P a). simpl in *.
+  rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto.
+  (** Bug omega: le "set" suivant ne devrait pas etre necessaire *)
+  set (u:= if eqA_dec a2 a then 1 else 0) in *; omega.
   right.
   inversion_clear H0; [|inversion H].
   split; auto.
   apply permut_length_1.
   red; red; intros.
-  generalize (P a); clear P; simpl.
-  destruct (eqA_dec a1 a) as [H2|H2];
-    destruct (eqA_dec b2 a) as [H3|H3]; auto.
-  simpl; rewrite <- plus_n_Sm; inversion 1; auto.
-  destruct H3; apply eqA_trans with a1; auto.
-  destruct H2; apply eqA_trans with b2; auto.
+  specialize (P a); simpl in *.
+  rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto.
+  (** Bug omega: idem *)
+  set (u:= if eqA_dec b2 a then 1 else 0) in *; omega.
 Qed.
 
 (** Permutation is compatible with length. *)
@@ -174,10 +217,7 @@ Proof.
   apply permut_tran with (a::l1); auto.
   revert H1; unfold Permutation.permutation, meq; simpl.
   intros; f_equal; auto.
-  destruct (eqA_dec b a0) as [H2|H2];
-    destruct (eqA_dec a a0) as [H3|H3]; auto.
-  destruct H3; apply eqA_trans with b; auto.
-  destruct H2; apply eqA_trans with a; auto.
+  rewrite (@if_eqA_rewrite_l a b a0); auto.
 Qed.
 
 Lemma NoDupA_equivlistA_permut :
@@ -196,13 +236,14 @@ Qed.
 Variable B : Type.
 Variable eqB : B->B->Prop.
 Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
-Variable eqB_trans : forall x y z, eqB x y -> eqB y z -> eqB x z.
+Variable eqB_trans : Transitive eqB.
+
 
 (** Permutation is compatible with map. *)
 
 Lemma permut_map :
   forall f,
-    (forall x y, eqA x y -> eqB (f x) (f y)) ->
+    (Proper (eqA==>eqB) f) ->
     forall l1 l2, permutation l1 l2 ->
       Permutation.permutation _ eqB_dec (map f l1) (map f l2).
 Proof.
@@ -220,8 +261,8 @@ Proof.
   intros; f_equal; auto.
   destruct (eqB_dec (f b) a0) as [H2|H2];
     destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
-  destruct H3; apply eqB_trans with (f b); auto.
-  destruct H2; apply eqB_trans with (f a); auto.
+  destruct H3; transitivity (f b); auto with *.
+  destruct H2; transitivity (f a); auto with *.
   apply permut_add_cons_inside.
   rewrite <- map_app.
   apply IHl1; auto.
@@ -229,10 +270,7 @@ Proof.
   apply permut_tran with (a::l1); auto.
   revert H1; unfold Permutation.permutation, meq; simpl.
   intros; f_equal; auto.
-  destruct (eqA_dec b a0) as [H2|H2];
-    destruct (eqA_dec a a0) as [H3|H3]; auto.
-  destruct H3; apply eqA_trans with b; auto.
-  destruct H2; apply eqA_trans with a; auto.
+  rewrite (@if_eqA_rewrite_l a b a0); auto.
 Qed.
 
 End Perm.
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 625f776bf..5b0fb21ef 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -96,6 +96,12 @@ Module KeyDecidableType(D:DecidableType).
   Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
   Hint Immediate eqk_sym eqke_sym.
 
+  Global Instance eqk_equiv : Equivalence eqk.
+  Proof. split; eauto. Qed.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+  Proof. split; eauto. Qed.
+
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
   Proof.
@@ -105,7 +111,7 @@ Module KeyDecidableType(D:DecidableType).
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
   Proof.
-   intros; apply InA_eqA with p; auto; apply eqk_trans; auto.
+   intros; apply InA_eqA with p; auto with *.
   Qed.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
@@ -128,7 +134,7 @@ Module KeyDecidableType(D:DecidableType).
 
   Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
   Proof.
-  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto.
+  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
   Qed.
 
   Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index e582db3ea..a8e1ebdd6 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -218,32 +218,32 @@ Notation Sort:=(sort lt).
 Notation NoDup:=(NoDupA eq).
 
 Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-Proof. exact (InA_eqA eq_sym eq_trans). Qed.
+Proof. exact (InA_eqA eq_equiv). Qed.
 
 Lemma ListIn_In : forall l x, List.In x l -> In x l.
-Proof. exact (In_InA eq_refl). Qed.
+Proof. exact (In_InA eq_equiv). Qed.
 
 Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_ltA lt_trans). Qed.
+Proof. exact (InfA_ltA lt_strorder). Qed.
 
 Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_lt). Qed.
+Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
 
 Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
-Proof. exact (SortA_InfA_InA eq_refl eq_sym lt_trans lt_eq eq_lt). Qed.
+Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
 
 Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.
 Proof. exact (@In_InfA t lt). Qed.
 
 Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.
-Proof. exact (InA_InfA eq_refl (ltA:=lt)). Qed.
+Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed.
 
 Lemma Inf_alt :
  forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
-Proof. exact (InfA_alt eq_refl eq_sym lt_trans lt_eq eq_lt). Qed.
+Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed.
 
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
-Proof. exact (SortA_NoDupA eq_refl eq_sym lt_trans lt_not_eq lt_eq eq_lt) . Qed.
+Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed.
 
 End ForNotations.
 
@@ -323,6 +323,30 @@ Module KeyOrderedType(O:OrderedType).
   Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
   Hint Immediate eqk_sym eqke_sym.
 
+  Global Instance eqk_equiv : Equivalence eqk.
+  Proof. split; eauto. Qed.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+  Proof. split; eauto. Qed.
+
+  Global Instance ltk_strorder : StrictOrder ltk.
+  Proof.
+   split; eauto.
+   intros (x,e); compute; apply (StrictOrder_Irreflexive x).
+  Qed.
+
+  Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
+  Proof.
+  intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+  Qed.
+
+  Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk.
+  Proof.
+  intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+  Qed.
+
   (* Additionnal facts *)
 
   Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'.
@@ -370,7 +394,7 @@ Module KeyOrderedType(O:OrderedType).
 
   Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
   Proof.
-  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto.
+  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
   Qed.
 
   Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
@@ -379,10 +403,10 @@ Module KeyOrderedType(O:OrderedType).
   Qed.
 
   Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
-  Proof. exact (InfA_eqA eqk_ltk). Qed.
+  Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed.
 
   Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
-  Proof. exact (InfA_ltA ltk_trans). Qed.
+  Proof. exact (InfA_ltA ltk_strorder). Qed.
 
   Hint Immediate Inf_eq.
   Hint Resolve Inf_lt.
@@ -390,7 +414,7 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Sort_Inf_In :
       forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
   Proof.
-  exact (SortA_InfA_InA eqk_refl eqk_sym ltk_trans ltk_eqk eqk_ltk).
+  exact (SortA_InfA_InA eqk_equiv ltk_strorder ltk_compat).
   Qed.
 
   Lemma Sort_Inf_NotIn :
@@ -405,7 +429,7 @@ Module KeyOrderedType(O:OrderedType).
 
   Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
   Proof.
-  exact (SortA_NoDupA eqk_refl eqk_sym ltk_trans ltk_not_eqk ltk_eqk eqk_ltk).
+  exact (SortA_NoDupA eqk_equiv ltk_strorder ltk_compat).
   Qed.
 
   Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 7258fe52f..fdb1ccc24 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Export SetoidList2 DecidableType2 OrderTac.
+Require Export SetoidList DecidableType2 OrderTac.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/theories.itarget b/theories/theories.itarget
index 0e0c27727..09aeac753 100644
--- a/theories/theories.itarget
+++ b/theories/theories.itarget
@@ -99,7 +99,6 @@ Lists/ListSet.vo
 Lists/ListTactics.vo
 Lists/List.vo
 Lists/SetoidList.vo
-Lists/SetoidList2.vo
 Lists/StreamMemo.vo
 Lists/Streams.vo
 Lists/TheoryList.vo