factorization part II (Properties + EqProperties), inclusion of FSetDecide (from A. Bohannon)

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

7 files changed, 2230 insertions, 2088 deletions

diff --git a/Makefile.common b/Makefile.common
index 0cfb0ed7d4..0e6c3925c6 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -571,7 +571,8 @@ FSETSBASEVO:=\
  theories/FSets/FMapWeakFacts.vo \
  theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo \
  theories/FSets/FMapWeak.vo          theories/FSets/FMapPositive.vo \
- theories/FSets/FMapIntMap.vo        theories/FSets/FSetToFiniteSet.vo
+ theories/FSets/FMapIntMap.vo        theories/FSets/FSetToFiniteSet.vo \
+ theories/FSets/FSetDecide.vo        theories/FSets/FSetWeakEqProperties.vo
 
 FSETS_basic:=
 
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
new file mode 100644
index 0000000000..825bdefedd
--- /dev/null
+++ b/theories/FSets/FSetDecide.v
@@ -0,0 +1,941 @@
+(***********************************************************************)
+(*  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$ *)
+
+(**************************************************************)
+(* FSetDecide.v                                               *)
+(*                                                            *)
+(* Author: Aaron Bohannon                                     *)
+(**************************************************************)
+
+(** This file implements a decision procedure for a certain
+    class of propositions involving finite sets.  *)
+
+Require Import Decidable DecidableTypeEx FSetWeakFacts.
+
+Module WeakDecide 
+ (Import M : FSetWeakInterface.S)
+ (D:DecidableType with Definition t:=M.E.t with Definition eq:=M.E.eq).
+
+(** * Overview
+    This functor defines the tactic [fsetdec], which will
+    solve any valid goal of the form
+<<
+    forall s1 ... sn,
+    forall x1 ... xm,
+    P1 -> ... -> Pk -> P
+>>
+    where [P]'s are defined by the grammar:
+<<
+
+P ::=
+| Q
+| Empty F
+| Subset F F'
+| Equal F F'
+
+Q ::=
+| E.eq X X'
+| In X F
+| Q /\ Q'
+| Q \/ Q'
+| Q -> Q'
+| Q <-> Q'
+| ~ Q
+| True
+| False
+
+F ::=
+| S
+| empty
+| singleton X
+| add X F
+| remove X F
+| union F F'
+| inter F F'
+| diff F F'
+
+X ::= x1 | ... | xm
+S ::= s1 | ... | sn
+
+>>
+
+The tactic will also work on some goals that vary slightly from
+the above form:
+- The variables and hypotheses may be mixed in any order and may
+  have already been introduced into the context.  Moreover,
+  there may be additional, unrelated hypotheses mixed in (these
+  will be ignored).
+- A conjunction of hypotheses will be handled as easily as
+  separate hypotheses, i.e., [P1 /\ P2 -> P] can be solved iff
+  [P1 -> P2 -> P] can be solved.
+- [fsetdec] should solve any goal if the FSet-related hypotheses
+  are contradictory.
+- [fsetdec] will first perform any necessary zeta and beta
+  reductions and will invoke [subst] to eliminate any Coq
+  equalities between finite sets or their elements.
+- If [E.eq] is convertible with Coq's equality, it will not
+  matter which one is used in the hypotheses or conclusion.
+- The tactic can solve goals where the finite sets or set
+  elements are expressed by Coq terms that are more complicated
+  than variables.  However, non-local definitions are not
+  expanded, and Coq equalities between non-variable terms are
+  not used.  For example, this goal will be solved:
+<<
+    forall (f : t -> t),
+    forall (g : elt -> elt),
+    forall (s1 s2 : t),
+    forall (x1 x2 : elt),
+    Equal s1 (f s2) ->
+    E.eq x1 (g (g x2)) ->
+    In x1 s1 ->
+    In (g (g x2)) (f s2)
+>>
+  This one will not be solved:
+<<
+    forall (f : t -> t),
+    forall (g : elt -> elt),
+    forall (s1 s2 : t),
+    forall (x1 x2 : elt),
+    Equal s1 (f s2) ->
+    E.eq x1 (g x2) ->
+    In x1 s1 ->
+    g x2 = g (g x2) ->
+    In (g (g x2)) (f s2)
+>>
+*)
+
+  (** * Facts and Tactics for Propositional Logic
+      These lemmas and tactics are in a module so that they do
+      not affect the namespace if you import the enclosing
+      module [Decide]. *)
+  Module FSetLogicalFacts.
+    Require Export Decidable.
+    Require Export Setoid.
+
+    (** ** Lemmas and Tactics About Decidable Propositions *)
+
+    (** ** Propositional Equivalences Involving Negation
+        These are all written with the unfolded form of
+        negation, since I am not sure if setoid rewriting will
+        always perform conversion. *)
+
+    (** ** Tactics for Negations *)
+
+    Tactic Notation "fold" "any" "not" :=
+      repeat (
+        match goal with
+        | H: context [?P -> False] |- _ =>
+          fold (~ P) in H
+        | |- context [?P -> False] =>
+          fold (~ P)
+        end).
+
+    (** [push not using db] will pushes all negations to the
+        leaves of propositions in the goal, using the lemmas in
+        [db] to assist in checking the decidability of the
+        propositions involved.  If [using db] is omitted, then
+        [core] will be used.  Additional versions are provided
+        to manipulate the hypotheses or the hypotheses and goal
+        together.
+
+        XXX: This tactic and the similar subsequent ones should
+        have been defined using [autorewrite].  However, there
+        is a bug in the order that Coq generates subgoals when
+        rewriting using a setoid.  In order to work around this
+        bug, these tactics had to be written out in an explicit
+        way.  When the bug is fixed these tactics will break!!
+        *)
+
+    Tactic Notation "push" "not" "using" ident(db) :=
+      unfold not, iff;
+      repeat (
+        match goal with
+        (** simplification by not_true_iff *)
+        | |- context [True -> False] =>
+          rewrite not_true_iff
+        (** simplification by not_false_iff *)
+        | |- context [False -> False] =>
+          rewrite not_false_iff
+        (** simplification by not_not_iff *)
+        | |- context [(?P -> False) -> False] =>
+          rewrite (not_not_iff P);
+            [ solve_decidable using db | ]
+        (** simplification by contrapositive *)
+        | |- context [(?P -> False) -> (?Q -> False)] =>
+          rewrite (contrapositive P Q);
+            [ solve_decidable using db | ]
+        (** simplification by or_not_l_iff_1/_2 *)
+        | |- context [(?P -> False) \/ ?Q] =>
+          (rewrite (or_not_l_iff_1 P Q);
+            [ solve_decidable using db | ]) ||
+          (rewrite (or_not_l_iff_2 P Q);
+            [ solve_decidable using db | ])
+        (** simplification by or_not_r_iff_1/_2 *)
+        | |- context [?P \/ (?Q -> False)] =>
+          (rewrite (or_not_r_iff_1 P Q);
+            [ solve_decidable using db | ]) ||
+          (rewrite (or_not_r_iff_2 P Q);
+            [ solve_decidable using db | ])
+        (** simplification by imp_not_l *)
+        | |- context [(?P -> False) -> ?Q] =>
+          rewrite (imp_not_l P Q);
+            [ solve_decidable using db | ]
+        (** rewriting by not_or_iff *)
+        | |- context [?P \/ ?Q -> False] =>
+          rewrite (not_or_iff P Q)
+        (** rewriting by not_and_iff *)
+        | |- context [?P /\ ?Q -> False] =>
+          rewrite (not_and_iff P Q)
+        (** rewriting by not_imp_iff *)
+        | |- context [(?P -> ?Q) -> False] =>
+          rewrite (not_imp_iff P Q);
+            [ solve_decidable using db | ]
+        end);
+      fold any not.
+
+    Tactic Notation "push" "not" :=
+      push not using core.
+
+    Tactic Notation
+      "push" "not" "in" "*" "|-" "using" ident(db) :=
+      unfold not, iff in * |-;
+      repeat (
+        match goal with
+        (** simplification by not_true_iff *)
+        | H: context [True -> False] |- _ =>
+          rewrite not_true_iff in H
+        (** simplification by not_false_iff *)
+        | H: context [False -> False] |- _ =>
+          rewrite not_false_iff in H
+        (** simplification by not_not_iff *)
+        | H: context [(?P -> False) -> False] |- _ =>
+          rewrite (not_not_iff P) in H;
+            [ | solve_decidable using db ]
+        (** simplification by contrapositive *)
+        | H: context [(?P -> False) -> (?Q -> False)] |- _ =>
+          rewrite (contrapositive P Q) in H;
+            [ | solve_decidable using db ]
+        (** simplification by or_not_l_iff_1/_2 *)
+        | H: context [(?P -> False) \/ ?Q] |- _ =>
+          (rewrite (or_not_l_iff_1 P Q) in H;
+            [ | solve_decidable using db ]) ||
+          (rewrite (or_not_l_iff_2 P Q) in H;
+            [ | solve_decidable using db ])
+        (** simplification by or_not_r_iff_1/_2 *)
+        | H: context [?P \/ (?Q -> False)] |- _ =>
+          (rewrite (or_not_r_iff_1 P Q) in H;
+            [ | solve_decidable using db ]) ||
+          (rewrite (or_not_r_iff_2 P Q) in H;
+            [ | solve_decidable using db ])
+        (** simplification by imp_not_l *)
+        | H: context [(?P -> False) -> ?Q] |- _ =>
+          rewrite (imp_not_l P Q) in H;
+            [ | solve_decidable using db ]
+        (** rewriting by not_or_iff *)
+        | H: context [?P \/ ?Q -> False] |- _ =>
+          rewrite (not_or_iff P Q) in H
+        (** rewriting by not_and_iff *)
+        | H: context [?P /\ ?Q -> False] |- _ =>
+          rewrite (not_and_iff P Q) in H
+        (** rewriting by not_imp_iff *)
+        | H: context [(?P -> ?Q) -> False] |- _ =>
+          rewrite (not_imp_iff P Q) in H;
+            [ | solve_decidable using db ]
+        end);
+      fold any not.
+
+    Tactic Notation "push" "not" "in" "*" "|-"  :=
+      push not in * |- using core.
+
+    Tactic Notation "push" "not" "in" "*" "using" ident(db) :=
+      push not using db; push not in * |- using db.
+    Tactic Notation "push" "not" "in" "*" :=
+      push not in * using core.
+
+    (** A simple test case to see how this works.  *)
+    Lemma test_push : forall P Q R : Prop,
+      decidable P ->
+      decidable Q ->
+      (~ True) ->
+      (~ False) ->
+      (~ ~ P) ->
+      (~ (P /\ Q) -> ~ R) ->
+      ((P /\ Q) \/ ~ R) ->
+      (~ (P /\ Q) \/ R) ->
+      (R \/ ~ (P /\ Q)) ->
+      (~ R \/ (P /\ Q)) ->
+      (~ P -> R) ->
+      (~ ((R -> P) \/ (R -> Q))) ->
+      (~ (P /\ R)) ->
+      (~ (P -> R)) ->
+      True.
+    Proof.
+      intros. push not in *. tauto.
+    Qed.
+
+    (** [pull not using db] will pull as many negations as
+        possible toward the top of the propositions in the goal,
+        using the lemmas in [db] to assist in checking the
+        decidability of the propositions involved.  If [using
+        db] is omitted, then [core] will be used.  Additional
+        versions are provided to manipulate the hypotheses or
+        the hypotheses and goal together. *)
+
+    Tactic Notation "pull" "not" "using" ident(db) :=
+      unfold not, iff;
+      repeat (
+        match goal with
+        (** simplification by not_true_iff *)
+        | |- context [True -> False] =>
+          rewrite not_true_iff
+        (** simplification by not_false_iff *)
+        | |- context [False -> False] =>
+          rewrite not_false_iff
+        (** simplification by not_not_iff *)
+        | |- context [(?P -> False) -> False] =>
+          rewrite (not_not_iff P);
+            [ solve_decidable using db | ]
+        (** simplification by contrapositive *)
+        | |- context [(?P -> False) -> (?Q -> False)] =>
+          rewrite (contrapositive P Q);
+            [ solve_decidable using db | ]
+        (** simplification by or_not_l_iff_1/_2 *)
+        | |- context [(?P -> False) \/ ?Q] =>
+          (rewrite (or_not_l_iff_1 P Q);
+            [ solve_decidable using db | ]) ||
+          (rewrite (or_not_l_iff_2 P Q);
+            [ solve_decidable using db | ])
+        (** simplification by or_not_r_iff_1/_2 *)
+        | |- context [?P \/ (?Q -> False)] =>
+          (rewrite (or_not_r_iff_1 P Q);
+            [ solve_decidable using db | ]) ||
+          (rewrite (or_not_r_iff_2 P Q);
+            [ solve_decidable using db | ])
+        (** simplification by imp_not_l *)
+        | |- context [(?P -> False) -> ?Q] =>
+          rewrite (imp_not_l P Q);
+            [ solve_decidable using db | ]
+        (** rewriting by not_or_iff *)
+        | |- context [(?P -> False) /\ (?Q -> False)] =>
+          rewrite <- (not_or_iff P Q)
+        (** rewriting by not_and_iff *)
+        | |- context [?P -> ?Q -> False] =>
+          rewrite <- (not_and_iff P Q)
+        (** rewriting by not_imp_iff *)
+        | |- context [?P /\ (?Q -> False)] =>
+          rewrite <- (not_imp_iff P Q);
+            [ solve_decidable using db | ]
+        (** rewriting by not_imp_rev_iff *)
+        | |- context [(?Q -> False) /\ ?P] =>
+          rewrite <- (not_imp_rev_iff P Q);
+            [ solve_decidable using db | ]
+        end);
+      fold any not.
+
+    Tactic Notation "pull" "not" :=
+      pull not using core.
+
+    Tactic Notation
+      "pull" "not" "in" "*" "|-" "using" ident(db) :=
+      unfold not, iff in * |-;
+      repeat (
+        match goal with
+        (** simplification by not_true_iff *)
+        | H: context [True -> False] |- _ =>
+          rewrite not_true_iff in H
+        (** simplification by not_false_iff *)
+        | H: context [False -> False] |- _ =>
+          rewrite not_false_iff in H
+        (** simplification by not_not_iff *)
+        | H: context [(?P -> False) -> False] |- _ =>
+          rewrite (not_not_iff P) in H;
+            [ | solve_decidable using db ]
+        (** simplification by contrapositive *)
+        | H: context [(?P -> False) -> (?Q -> False)] |- _ =>
+          rewrite (contrapositive P Q) in H;
+            [ | solve_decidable using db ]
+        (** simplification by or_not_l_iff_1/_2 *)
+        | H: context [(?P -> False) \/ ?Q] |- _ =>
+          (rewrite (or_not_l_iff_1 P Q) in H;
+            [ | solve_decidable using db ]) ||
+          (rewrite (or_not_l_iff_2 P Q) in H;
+            [ | solve_decidable using db ])
+        (** simplification by or_not_r_iff_1/_2 *)
+        | H: context [?P \/ (?Q -> False)] |- _ =>
+          (rewrite (or_not_r_iff_1 P Q) in H;
+            [ | solve_decidable using db ]) ||
+          (rewrite (or_not_r_iff_2 P Q) in H;
+            [ | solve_decidable using db ])
+        (** simplification by imp_not_l *)
+        | H: context [(?P -> False) -> ?Q] |- _ =>
+          rewrite (imp_not_l P Q) in H;
+            [ | solve_decidable using db ]
+        (** rewriting by not_or_iff *)
+        | H: context [(?P -> False) /\ (?Q -> False)] |- _ =>
+          rewrite <- (not_or_iff P Q) in H
+        (** rewriting by not_and_iff *)
+        | H: context [?P -> ?Q -> False] |- _ =>
+          rewrite <- (not_and_iff P Q) in H
+        (** rewriting by not_imp_iff *)
+        | H: context [?P /\ (?Q -> False)] |- _ =>
+          rewrite <- (not_imp_iff P Q) in H;
+            [ | solve_decidable using db ]
+        (** rewriting by not_imp_rev_iff *)
+        | H: context [(?Q -> False) /\ ?P] |- _ =>
+          rewrite <- (not_imp_rev_iff P Q) in H;
+            [ | solve_decidable using db ]
+        end);
+      fold any not.
+
+    Tactic Notation "pull" "not" "in" "*" "|-"  :=
+      pull not in * |- using core.
+
+    Tactic Notation "pull" "not" "in" "*" "using" ident(db) :=
+      pull not using db; pull not in * |- using db.
+    Tactic Notation "pull" "not" "in" "*" :=
+      pull not in * using core.
+
+    (** A simple test case to see how this works.  *)
+    Lemma test_pull : forall P Q R : Prop,
+      decidable P ->
+      decidable Q ->
+      (~ True) ->
+      (~ False) ->
+      (~ ~ P) ->
+      (~ (P /\ Q) -> ~ R) ->
+      ((P /\ Q) \/ ~ R) ->
+      (~ (P /\ Q) \/ R) ->
+      (R \/ ~ (P /\ Q)) ->
+      (~ R \/ (P /\ Q)) ->
+      (~ P -> R) ->
+      (~ (R -> P) /\ ~ (R -> Q)) ->
+      (~ P \/ ~ R) ->
+      (P /\ ~ R) ->
+      (~ R /\ P) ->
+      True.
+    Proof.
+      intros. pull not in *. tauto.
+    Qed.
+
+  End FSetLogicalFacts.
+  Import FSetLogicalFacts.
+
+  (** * Auxiliary Tactics
+      Again, these lemmas and tactics are in a module so that
+      they do not affect the namespace if you import the
+      enclosing module [Decide].  *)
+  Module FSetDecideAuxiliary.
+
+    (** ** Generic Tactics
+        We begin by defining a few generic, useful tactics. *)
+
+    (** [if t then t1 else t2] executes [t] and, if it does not
+        fail, then [t1] will be applied to all subgoals
+        produced.  If [t] fails, then [t2] is executed. *)
+    Tactic Notation
+      "if" tactic(t)
+      "then" tactic(t1)
+      "else" tactic(t2) :=
+      first [ t; first [ t1 | fail 2 ] | t2 ].
+
+    (** [prop P holds by t] succeeds (but does not modify the
+        goal or context) if the proposition [P] can be proved by
+        [t] in the current context.  Otherwise, the tactic
+        fails. *)
+    Tactic Notation "prop" constr(P) "holds" "by" tactic(t) :=
+      let H := fresh in
+      assert P as H by t;
+      clear H.
+
+    (** This tactic acts just like [assert ... by ...] but will
+        fail if the context already contains the proposition. *)
+    Tactic Notation "assert" "new" constr(e) "by" tactic(t) :=
+      match goal with
+      | H: e |- _ => fail 1
+      | _ => assert e by t
+      end.
+
+    (** [subst++] is similar to [subst] except that
+        - it never fails (as [subst] does on recursive
+          equations),
+        - it substitutes locally defined variable for their
+          definitions,
+        - it performs beta reductions everywhere, which may
+          arise after substituting a locally defined function
+          for its definition.
+        *)
+    Tactic Notation "subst" "++" :=
+      repeat (
+        match goal with
+        | x : _ |- _ => subst x
+        end);
+      cbv zeta beta in *.
+
+    (** If you have a negated goal and [H] is a negated
+        hypothesis, then [contra H] exchanges your goal and [H],
+        removing the negations.  (Just like [swap] but reuses
+        the same name. *)
+    Ltac contra H :=
+      let J := fresh in
+      unfold not;
+      unfold not in H;
+      intros J;
+      apply H;
+      clear H;
+      rename J into H.
+
+    (** [decompose records] calls [decompose record H] on every
+        relevant hypothesis [H]. *)
+    Tactic Notation "decompose" "records" :=
+      repeat (
+        match goal with
+        | H: _ |- _ => progress (decompose record H); clear H
+        end).
+
+    (** ** Discarding Irrelevant Hypotheses
+        We will want to clear the context of any
+        non-FSet-related hypotheses in order to increase the
+        speed of the tactic.  To do this, we will need to be
+        able to decide which are relevant.  We do this by making
+        a simple inductive definition classifying the
+        propositions of interest. *)
+
+    Inductive FSet_elt_Prop : Prop -> Prop :=
+    | eq_Prop : forall (S : Set) (x y : S),
+        FSet_elt_Prop (x = y)
+    | eq_elt_prop : forall x y,
+        FSet_elt_Prop (E.eq x y)
+    | In_elt_prop : forall x s,
+        FSet_elt_Prop (In x s)
+    | True_elt_prop :
+        FSet_elt_Prop True
+    | False_elt_prop :
+        FSet_elt_Prop False
+    | conj_elt_prop : forall P Q,
+        FSet_elt_Prop P ->
+        FSet_elt_Prop Q ->
+        FSet_elt_Prop (P /\ Q)
+    | disj_elt_prop : forall P Q,
+        FSet_elt_Prop P ->
+        FSet_elt_Prop Q ->
+        FSet_elt_Prop (P \/ Q)
+    | impl_elt_prop : forall P Q,
+        FSet_elt_Prop P ->
+        FSet_elt_Prop Q ->
+        FSet_elt_Prop (P -> Q)
+    | not_elt_prop : forall P,
+        FSet_elt_Prop P ->
+        FSet_elt_Prop (~ P).
+
+    Inductive FSet_Prop : Prop -> Prop :=
+    | elt_FSet_Prop : forall P,
+        FSet_elt_Prop P ->
+        FSet_Prop P
+    | Empty_FSet_Prop : forall s,
+        FSet_Prop (Empty s)
+    | Subset_FSet_Prop : forall s1 s2,
+        FSet_Prop (Subset s1 s2)
+    | Equal_FSet_Prop : forall s1 s2,
+        FSet_Prop (Equal s1 s2).
+
+    (** Here is the tactic that will throw away hypotheses that
+        are not useful (for the intended scope of the [fsetdec]
+        tactic). *)
+    Hint Constructors FSet_elt_Prop FSet_Prop : FSet_Prop.
+    Ltac discard_nonFSet :=
+      decompose records;
+      repeat (
+        match goal with
+        | H : ?P |- _ =>
+          if prop (FSet_Prop P) holds by
+            (auto 100 with FSet_Prop)
+          then fail
+          else clear H
+        end).
+
+    (** ** Turning Set Operators into Propositional Connectives
+        The lemmas from [FSetFacts] will be used to break down
+        set operations into propositional formulas built over
+        the predicates [In] and [E.eq] applied only to
+        variables.  We are going to use them with [autorewrite].
+        *)
+    Module F := FSetWeakFacts.Facts M D.
+    Hint Rewrite
+      F.empty_iff F.singleton_iff F.add_iff F.remove_iff
+      F.union_iff F.inter_iff F.diff_iff
+    : set_simpl.
+
+    (** ** Decidability of FSet Propositions *)
+
+    (** [In] is decidable. *)
+    Lemma dec_In : forall x s,
+      decidable (In x s).
+    Proof.
+      red; intros; generalize (F.mem_iff s x); case (mem x s); intuition.
+    Qed.
+
+    (** [E.eq] is decidable. *)
+    Lemma dec_eq : forall (x y : E.t),
+      decidable (E.eq x y).
+    Proof.
+      red; intros x y; destruct (D.eq_dec x y); auto.
+    Qed.
+
+    (** The hint database [FSet_decidability] will be given to
+        the [push_neg] tactic from the module [Negation]. *)
+    Hint Resolve dec_In dec_eq : FSet_decidability.
+
+    (** ** Normalizing Propositions About Equality
+        We have to deal with the fact that [E.eq] may be
+        convertible with Coq's equality.  Thus, we will find the
+        following tactics useful to replace one form with the
+        other everywhere. *)
+
+    (** The next tactic, [Logic_eq_to_E_eq], mentions the term
+        [E.t]; thus, we must ensure that [E.t] is used in favor
+        of any other convertible but syntactically distinct
+        term. *)
+    Ltac change_to_E_t :=
+      repeat (
+        match goal with
+        | H : ?T |- _ =>
+          progress (change T with E.t in H);
+          repeat (
+            match goal with
+            | J : _ |- _ => progress (change T with E.t in J)
+            | |- _ => progress (change T with E.t)
+            end )
+        end).
+
+    (** These two tactics take us from Coq's built-in equality
+        to [E.eq] (and vice versa) when possible. *)
+
+    Ltac Logic_eq_to_E_eq :=
+      repeat (
+        match goal with
+        | H: _ |- _ =>
+          progress (change (@Logic.eq E.t) with E.eq in H)
+        | |- _ =>
+          progress (change (@Logic.eq E.t) with E.eq)
+        end).
+
+    Ltac E_eq_to_Logic_eq :=
+      repeat (
+        match goal with
+        | H: _ |- _ =>
+          progress (change E.eq with (@Logic.eq E.t) in H)
+        | |- _ =>
+          progress (change E.eq with (@Logic.eq E.t))
+        end).
+
+    (** This tactic works like the built-in tactic [subst], but
+        at the level of set element equality (which may not be
+        the convertible with Coq's equality). *)
+    Ltac substFSet :=
+      repeat (
+        match goal with
+        | H: E.eq ?x ?y |- _ => rewrite H in *; clear H
+        end).
+
+    (** ** Considering Decidability of Base Propositions
+        This tactic adds assertions about the decidability of
+        [E.eq] and [In] to the context.  This is necessary for
+        the completeness of the [fsetdec] tactic.  However, in
+        order to minimize the cost of proof search, we should be
+        careful to not add more than we need.  Once negations
+        have been pushed to the leaves of the propositions, we
+        only need to worry about decidability for those base
+        propositions that appear in a negated form. *)
+    Ltac assert_decidability :=
+      (** We actually don't want these rules to fire if the
+          syntactic context in the patterns below is trivially
+          empty, but we'll just do some clean-up at the
+          afterward.  *)
+      repeat (
+        match goal with
+        | H: context [~ E.eq ?x ?y] |- _ =>
+          assert new (E.eq x y \/ ~ E.eq x y) by (apply dec_eq)
+        | H: context [~ In ?x ?s] |- _ =>
+          assert new (In x s \/ ~ In x s) by (apply dec_In)
+        | |- context [~ E.eq ?x ?y] =>
+          assert new (E.eq x y \/ ~ E.eq x y) by (apply dec_eq)
+        | |- context [~ In ?x ?s] =>
+          assert new (In x s \/ ~ In x s) by (apply dec_In)
+        end);
+      (** Now we eliminate the useless facts we added (because
+          they would likely be very harmful to performance). *)
+      repeat (
+        match goal with
+        | _: ~ ?P, H : ?P \/ ~ ?P |- _ => clear H
+        end).
+
+    (** ** Handling [Empty], [Subset], and [Equal]
+        This tactic instantiates universally quantified
+        hypotheses (which arise from the unfolding of [Empty],
+        [Subset], and [Equal]) for each of the set element
+        expressions that is involved in some membership or
+        equality fact.  Then it throws away those hypotheses,
+        which should no longer be needed. *)
+    Ltac inst_FSet_hypotheses :=
+      repeat (
+        match goal with
+        | H : forall a : E.t, _,
+          _ : context [ In ?x _ ] |- _ =>
+          let P := type of (H x) in
+          assert new P by (exact (H x))
+        | H : forall a : E.t, _
+          |- context [ In ?x _ ] =>
+          let P := type of (H x) in
+          assert new P by (exact (H x))
+        | H : forall a : E.t, _,
+          _ : context [ E.eq ?x _ ] |- _ =>
+          let P := type of (H x) in
+          assert new P by (exact (H x))
+        | H : forall a : E.t, _
+          |- context [ E.eq ?x _ ] =>
+          let P := type of (H x) in
+          assert new P by (exact (H x))
+        | H : forall a : E.t, _,
+          _ : context [ E.eq _ ?x ] |- _ =>
+          let P := type of (H x) in
+          assert new P by (exact (H x))
+        | H : forall a : E.t, _
+          |- context [ E.eq _ ?x ] =>
+          let P := type of (H x) in
+          assert new P by (exact (H x))
+        end);
+      repeat (
+        match goal with
+        | H : forall a : E.t, _ |- _ =>
+          clear H
+        end).
+
+    (** ** The Core [fsetdec] Auxiliary Tactics *)
+
+    (** Here is the crux of the proof search.  Recursion through
+        [intuition]!  (This will terminate if I correctly
+        understand the behavior of [intuition].) *)
+    Ltac fsetdec_rec :=
+      try (match goal with
+      | H: E.eq ?x ?x -> False |- _ => destruct H
+      end);
+      (reflexivity ||
+      contradiction ||
+      (progress substFSet; intuition fsetdec_rec)).
+
+    (** If we add [unfold Empty, Subset, Equal in *; intros;] to
+        the beginning of this tactic, it will satisfy the same
+        specification as the [fsetdec] tactic; however, it will
+        be much slower than necessary without the pre-processing
+        done by the wrapper tactic [fsetdec]. *)
+    Ltac fsetdec_body :=
+      inst_FSet_hypotheses;
+      autorewrite with set_simpl in *;
+      push not in * using FSet_decidability;
+      substFSet;
+      assert_decidability;
+      auto using E.eq_refl;
+      (intuition fsetdec_rec) ||
+      fail 1
+        "because the goal is beyond the scope of this tactic".
+
+  End FSetDecideAuxiliary.
+  Import FSetDecideAuxiliary.
+
+  (** * The [fsetdec] Tactic
+      Here is the top-level tactic (the only one intended for
+      clients of this library).  It's specification is given at
+      the top of the file. *)
+  Ltac fsetdec :=
+    (** We first unfold any occurrences of [iff]. *)
+    unfold iff in *;
+    (** We fold occurrences of [not] because it is better for
+        [intros] to leave us with a goal of [~ P] than a goal of
+        [False]. *)
+    fold any not; intros;
+    (** Now we decompose conjunctions, which will allow the
+        [discard_nonFSet] and [assert_decidability] tactics to
+        do a much better job. *)
+    decompose records;
+    discard_nonFSet;
+    (** We unfold these defined propositions on finite sets.  If
+        our goal was one of them, then have one more item to
+        introduce now. *)
+    unfold Empty, Subset, Equal in *; intros;
+    (** We now want to get rid of all uses of [=] in favor of
+        [E.eq].  However, the best way to eliminate a [=] is in
+        the context is with [subst], so we will try that first.
+        In fact, we may as well convert uses of [E.eq] into [=]
+        when possible before we do [subst] so that we can even
+        more mileage out of it.  Then we will convert all
+        remaining uses of [=] back to [E.eq] when possible.  We
+        use [change_to_E_t] to ensure that we have a canonical
+        name for set elements, so that [Logic_eq_to_E_eq] will
+        work properly.  *)
+    change_to_E_t; E_eq_to_Logic_eq; subst++; Logic_eq_to_E_eq;
+    (** The next optimization is to swap a negated goal with a
+        negated hypothesis when possible.  Any swap will improve
+        performance by eliminating the total number of
+        negations, but we will get the maximum benefit if we
+        swap the goal with a hypotheses mentioning the same set
+        element, so we try that first.  If we reach the fourth
+        branch below, we attempt any swap.  However, to maintain
+        completeness of this tactic, we can only perform such a
+        swap with a decidable proposition; hence, we first test
+        whether the hypothesis is an [FSet_elt_Prop], noting
+        that any [FSet_elt_Prop] is decidable. *)
+    pull not using FSet_decidability;
+    unfold not in *;
+    match goal with
+    | H: (In ?x ?r) -> False |- (In ?x ?s) -> False =>
+      contra H; fsetdec_body
+    | H: (In ?x ?r) -> False |- (E.eq ?x ?y) -> False =>
+      contra H; fsetdec_body
+    | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
+      contra H; fsetdec_body
+    | H: ?P -> False |- ?Q -> False =>
+      if prop (FSet_elt_Prop P) holds by
+        (auto 100 with FSet_Prop)
+      then (contra H; fsetdec_body)
+      else fsetdec_body
+    | |- _ =>
+      fsetdec_body
+    end.
+
+  (** * Examples *)
+
+  Module FSetDecideTestCases.
+
+    Lemma test_eq_trans_1 : forall x y z s,
+      E.eq x y ->
+      ~ ~ E.eq z y ->
+      In x s ->
+      In z s.
+    Proof. fsetdec. Qed.
+
+    Lemma test_eq_trans_2 : forall x y z r s,
+      In x (singleton y) ->
+      ~ In z r ->
+      ~ ~ In z (add y r) ->
+      In x s ->
+      In z s.
+    Proof. fsetdec. Qed.
+
+    Lemma test_eq_neq_trans_1 : forall w x y z s,
+      E.eq x w ->
+      ~ ~ E.eq x y ->
+      ~ E.eq y z ->
+      In w s ->
+      In w (remove z s).
+    Proof. fsetdec. Qed.
+
+    Lemma test_eq_neq_trans_2 : forall w x y z r1 r2 s,
+      In x (singleton w) ->
+      ~ In x r1 ->
+      In x (add y r1) ->
+      In y r2 ->
+      In y (remove z r2) ->
+      In w s ->
+      In w (remove z s).
+    Proof. fsetdec. Qed.
+
+    Lemma test_In_singleton : forall x,
+      In x (singleton x).
+    Proof. fsetdec. Qed.
+
+    Lemma test_Subset_add_remove : forall x s,
+      s [<=] (add x (remove x s)).
+    Proof. fsetdec. Qed.
+
+    Lemma test_eq_disjunction : forall w x y z,
+      In w (add x (add y (singleton z))) ->
+      E.eq w x \/ E.eq w y \/ E.eq w z.
+    Proof. fsetdec. Qed.
+
+    Lemma test_not_In_disj : forall x y s1 s2 s3 s4,
+      ~ In x (union s1 (union s2 (union s3 (add y s4)))) ->
+      ~ (In x s1 \/ In x s4 \/ E.eq y x).
+    Proof. fsetdec. Qed.
+
+    Lemma test_not_In_conj : forall x y s1 s2 s3 s4,
+      ~ In x (union s1 (union s2 (union s3 (add y s4)))) ->
+      ~ In x s1 /\ ~ In x s4 /\ ~ E.eq y x.
+    Proof. fsetdec. Qed.
+
+    Lemma test_iff_conj : forall a x s s',
+    (In a s' <-> E.eq x a \/ In a s) ->
+    (In a s' <-> In a (add x s)).
+    Proof. fsetdec. Qed.
+
+    Lemma test_set_ops_1 : forall x q r s,
+      (singleton x) [<=] s ->
+      Empty (union q r) ->
+      Empty (inter (diff s q) (diff s r)) ->
+      ~ In x s.
+    Proof. fsetdec. Qed.
+
+    Lemma eq_chain_test : forall x1 x2 x3 x4 s1 s2 s3 s4,
+      Empty s1 ->
+      In x2 (add x1 s1) ->
+      In x3 s2 ->
+      ~ In x3 (remove x2 s2) ->
+      ~ In x4 s3 ->
+      In x4 (add x3 s3) ->
+      In x1 s4 ->
+      Subset (add x4 s4) s4.
+    Proof. fsetdec. Qed.
+
+    Lemma test_too_complex : forall x y z r s,
+      E.eq x y ->
+      (In x (singleton y) -> r [<=] s) ->
+      In z r ->
+      In z s.
+    Proof.
+      (** [fsetdec] is not intended to solve this directly. *)
+      intros until s; intros Heq H Hr; lapply H; fsetdec.
+    Qed.
+
+    Lemma function_test_1 :
+      forall (f : t -> t),
+      forall (g : elt -> elt),
+      forall (s1 s2 : t),
+      forall (x1 x2 : elt),
+      Equal s1 (f s2) ->
+      E.eq x1 (g (g x2)) ->
+      In x1 s1 ->
+      In (g (g x2)) (f s2).
+    Proof. fsetdec. Qed.
+
+    Lemma function_test_2 :
+      forall (f : t -> t),
+      forall (g : elt -> elt),
+      forall (s1 s2 : t),
+      forall (x1 x2 : elt),
+      Equal s1 (f s2) ->
+      E.eq x1 (g x2) ->
+      In x1 s1 ->
+      g x2 = g (g x2) ->
+      In (g (g x2)) (f s2).
+    Proof.
+      (** [fsetdec] is not intended to solve this directly. *)
+      intros until 3. intros g_eq. rewrite <- g_eq. fsetdec.
+    Qed.
+
+  End FSetDecideTestCases.
+
+End WeakDecide.
+
+Require Import FSetInterface.
+
+Module Decide (M : FSetInterface.S).
+  Module D:=OT_as_DT M.E.
+  Module WD := WeakDecide M D.
+  Ltac fsetdec := WD.fsetdec.
+End Decide.
\ No newline at end of file
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 25187da6d2..89fae94e6f 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -12,926 +12,20 @@
 
 (** This module proves many properties of finite sets that 
     are consequences of the axiomatization in [FsetInterface] 
-    Contrary to the functor in [FsetProperties] it uses 
+    Contrary to the functor in [FsetWeakProperties] it uses 
     sets operations instead of predicates over sets, i.e.
     [mem x s=true] instead of [In x s], 
     [equal s s'=true] instead of [Equal s s'], etc. *)
 
+Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.
 
-Require Import FSetProperties.
-Require Import Zerob.
-Require Import Sumbool.
-Require Import Omega.
+(** Since the properties that used to be there do not depend on 
+    the element ordering, we now simply import them from 
+    FSetWeakEqProperties *)
 
-Module EqProperties (M:S).
-Import M.
-Import Logic. (* to unmask [eq] *)  
-Import Peano. (* to unmask [lt] *)
-  
-Module ME := OrderedTypeFacts E.  
-Module MP := Properties M.
-Import MP.
-Import MP.FM.
-
-Definition Add := MP.Add.
-
-Section BasicProperties. 
-
-(** Some old specifications written with boolean equalities. *) 
-
-Variable s s' s'': t.
-Variable x y z : elt.
-
-Lemma mem_eq: 
-  E.eq x y -> mem x s=mem y s.
-Proof. 
-intro H; rewrite H; auto.
-Qed.
-
-Lemma equal_mem_1: 
-  (forall a, mem a s=mem a s') -> equal s s'=true.
-Proof. 
-intros; apply equal_1; unfold Equal; intros.
-do 2 rewrite mem_iff; rewrite H; tauto.
-Qed.
-
-Lemma equal_mem_2: 
-  equal s s'=true -> forall a, mem a s=mem a s'.
-Proof. 
-intros; rewrite (equal_2 H); auto.
-Qed.
-
-Lemma subset_mem_1: 
-  (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
-Proof. 
-intros; apply subset_1; unfold Subset; intros a.
-do 2 rewrite mem_iff; auto.
-Qed.
-
-Lemma subset_mem_2: 
-  subset s s'=true -> forall a, mem a s=true -> mem a s'=true.
-Proof. 
-intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
-Qed.
-  
-Lemma empty_mem: mem x empty=false.
-Proof. 
-rewrite <- not_mem_iff; auto with set.
-Qed.
-
-Lemma is_empty_equal_empty: is_empty s = equal s empty.
-Proof. 
-apply bool_1; split; intros.
-rewrite <- (empty_is_empty_1 (s:=empty)); auto with set.
-rewrite <- is_empty_iff; auto with set.
-Qed.
-  
-Lemma choose_mem_1: choose s=Some x -> mem x s=true.
-Proof.  
-auto with set.
-Qed.
-
-Lemma choose_mem_2: choose s=None -> is_empty s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma add_mem_1: mem x (add x s)=true.
-Proof.
-auto with set.
-Qed.  
- 
-Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
-Proof. 
-apply add_neq_b.
-Qed.
-
-Lemma remove_mem_1: mem x (remove x s)=false.
-Proof. 
-rewrite <- not_mem_iff; auto with set.
-Qed. 
- 
-Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
-Proof. 
-apply remove_neq_b.
-Qed.
-
-Lemma singleton_equal_add: 
-  equal (singleton x) (add x empty)=true.
-Proof.
-rewrite (singleton_equal_add x); auto with set.
-Qed.  
-
-Lemma union_mem: 
-  mem x (union s s')=mem x s || mem x s'.
-Proof. 
-apply union_b.
-Qed.
-
-Lemma inter_mem: 
-  mem x (inter s s')=mem x s && mem x s'.
-Proof. 
-apply inter_b.
-Qed.
-
-Lemma diff_mem: 
-  mem x (diff s s')=mem x s && negb (mem x s').
-Proof. 
-apply diff_b.
-Qed.
-
-(** properties of [mem] *)
-
-Lemma mem_3 : ~In x s -> mem x s=false.
-Proof.
-intros; rewrite <- not_mem_iff; auto.
-Qed.
-
-Lemma mem_4 : mem x s=false -> ~In x s.
-Proof.
-intros; rewrite not_mem_iff; auto.
-Qed.
-
-(** Properties of [equal] *) 
-
-Lemma equal_refl: equal s s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma equal_sym: equal s s'=equal s' s.
-Proof.
-intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
-Qed.
-
-Lemma equal_trans: 
- equal s s'=true -> equal s' s''=true -> equal s s''=true.
-Proof.
-intros; rewrite (equal_2 H); auto.
-Qed.
-
-Lemma equal_equal: 
- equal s s'=true -> equal s s''=equal s' s''.
-Proof.
-intros; rewrite (equal_2 H); auto.
-Qed.
-
-Lemma equal_cardinal: 
- equal s s'=true -> cardinal s=cardinal s'.
-Proof.
-auto with set.
-Qed.
-
-(* Properties of [subset] *)
-
-Lemma subset_refl: subset s s=true. 
-Proof.
-auto with set.
-Qed.
-
-Lemma subset_antisym: 
- subset s s'=true -> subset s' s=true -> equal s s'=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma subset_trans: 
- subset s s'=true -> subset s' s''=true -> subset s s''=true.
-Proof.
-do 3 rewrite <- subset_iff; intros.
-apply subset_trans with s'; auto.
-Qed.
-
-Lemma subset_equal: 
- equal s s'=true -> subset s s'=true.
-Proof.
-auto with set.
-Qed.
-
-(** Properties of [choose] *)
-
-Lemma choose_mem_3: 
- is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
-Proof.
-intros.
-generalize (@choose_1 s) (@choose_2 s).
-destruct (choose s);intros.
-exists e;auto with set.
-generalize (H1 (refl_equal None)); clear H1.
-intros; rewrite (is_empty_1 H1) in H; discriminate.
-Qed.
-
-Lemma choose_mem_4: choose empty=None.
-Proof.
-generalize (@choose_1 empty).
-case (@choose empty);intros;auto.
-elim (@empty_1 e); auto.
-Qed.
-
-(** Properties of [add] *)
-
-Lemma add_mem_3: 
- mem y s=true -> mem y (add x s)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma add_equal: 
- mem x s=true -> equal (add x s) s=true.
-Proof.
-auto with set.
-Qed.
-
-(** Properties of [remove] *)
-
-Lemma remove_mem_3: 
- mem y (remove x s)=true -> mem y s=true.
-Proof.
-rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
-Qed.
-
-Lemma remove_equal: 
- mem x s=false -> equal (remove x s) s=true.
-Proof.
-intros; apply equal_1; apply remove_equal.
-rewrite not_mem_iff; auto.
-Qed.
-
-Lemma add_remove: 
- mem x s=true -> equal (add x (remove x s)) s=true.
-Proof.
-intros; apply equal_1; apply add_remove; auto with set.
-Qed.
-
-Lemma remove_add: 
- mem x s=false -> equal (remove x (add x s)) s=true.
-Proof.
-intros; apply equal_1; apply remove_add; auto.
-rewrite not_mem_iff; auto.
-Qed.
-
-(** Properties of [is_empty] *)
-
-Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
-Proof.
-intros; apply bool_1; split; intros.
-rewrite cardinal_1; simpl; auto with set.
-assert (cardinal s = 0) by (apply zerob_true_elim; auto).
-auto with set.
-Qed.
-
-(** Properties of [singleton] *)
-
-Lemma singleton_mem_1: mem x (singleton x)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
-Proof.
-intros; rewrite singleton_b.
-unfold eqb; destruct (eq_dec x y); intuition.
-Qed.
-
-Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
-Proof.
-intros; apply singleton_1; auto with set.
-Qed.
-
-(** Properties of [union] *)
-
-Lemma union_sym:
- equal (union s s') (union s' s)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_subset_equal: 
- subset s s'=true -> equal (union s s') s'=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_equal_1: 
- equal s s'=true-> equal (union s s'') (union s' s'')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_equal_2: 
- equal s' s''=true-> equal (union s s') (union s s'')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_assoc: 
- equal (union (union s s') s'') (union s (union s' s''))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma add_union_singleton: 
- equal (add x s) (union (singleton x) s)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_add: 
- equal (union (add x s) s') (add x (union s s'))=true.
-Proof.
-auto with set.
-Qed.
-
-(* caracterisation of [union] via [subset] *)
-
-Lemma union_subset_1: subset s (union s s')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_subset_2: subset s' (union s s')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_subset_3:
- subset s s''=true -> subset s' s''=true -> 
-  subset (union s s') s''=true.
-Proof.
-intros; apply subset_1; apply union_subset_3; auto with set.
-Qed.
-
-(** Properties of [inter] *) 
-
-Lemma inter_sym: equal (inter s s') (inter s' s)=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_subset_equal: 
- subset s s'=true -> equal (inter s s') s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_equal_1: 
- equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_equal_2: 
- equal s' s''=true -> equal (inter s s') (inter s s'')=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_assoc: 
- equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_inter_1: 
- equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma union_inter_2: 
- equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_add_1: mem x s'=true -> 
- equal (inter (add x s) s') (add x (inter s s'))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_add_2: mem x s'=false -> 
- equal (inter (add x s) s') (inter s s')=true.
-Proof.
-intros; apply equal_1; apply inter_add_2.
-rewrite not_mem_iff; auto.
-Qed.
+Require FSetWeakEqProperties.
 
-(* caracterisation of [union] via [subset] *)
-
-Lemma inter_subset_1: subset (inter s s') s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_subset_2: subset (inter s s') s'=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma inter_subset_3:
- subset s'' s=true -> subset s'' s'=true -> 
-  subset s'' (inter s s')=true.
-Proof.
-intros; apply subset_1; apply inter_subset_3; auto with set.
-Qed.
-
-(** Properties of [diff] *)
-
-Lemma diff_subset: subset (diff s s') s=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma diff_subset_equal:
- subset s s'=true -> equal (diff s s') empty=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma remove_inter_singleton: 
- equal (remove x s) (diff s (singleton x))=true.
-Proof.
-auto with set.
-Qed.
-
-Lemma diff_inter_empty:
- equal (inter (diff s s') (inter s s')) empty=true. 
-Proof.
-auto with set.
-Qed.
-
-Lemma diff_inter_all: 
- equal (union (diff s s') (inter s s')) s=true.
-Proof.
-auto with set.
-Qed.
-
-End BasicProperties.
-
-Hint Immediate empty_mem is_empty_equal_empty add_mem_1
-   remove_mem_1 singleton_equal_add union_mem inter_mem
-   diff_mem equal_sym add_remove remove_add : set. 
-Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
-   choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
-   subset_refl subset_equal subset_antisym
-   add_mem_3 add_equal remove_mem_3 remove_equal : set.
-
-
-(** General recursion principle *)
-
-Lemma set_rec:  forall (P:t->Type),
- (forall s s', equal s s'=true -> P s -> P s') -> 
- (forall s x, mem x s=false -> P s -> P (add x s)) -> 
- P empty -> forall s, P s.
-Proof.
-intros.
-apply set_induction; auto; intros.
-apply X with empty; auto with set.
-apply X with (add x s0); auto with set.
-apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto.
-apply X0; auto with set; apply mem_3; auto.
-Qed.
-
-(** Properties of [fold] *)
-
-Lemma exclusive_set : forall s s' x,
- ~(In x s/\In x s') <-> mem x s && mem x s'=false.
-Proof.
-intros; do 2 rewrite mem_iff.
-destruct (mem x s); destruct (mem x s'); intuition.
-Qed.
-
-Section Fold. 
-Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
-Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
-Variables (i:A).
-Variables (s s':t)(x:elt).
- 
-Lemma fold_empty: eqA (fold f empty i) i.
-Proof. 
-apply fold_empty; auto.
-Qed.
-
-Lemma fold_equal: 
- equal s s'=true -> eqA (fold f s i) (fold f s' i).
-Proof. 
-intros; apply fold_equal with (eqA:=eqA); auto with set.
-Qed.
-   
-Lemma fold_add: 
- mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
-Proof. 
-intros; apply fold_add with (eqA:=eqA); auto.
-rewrite not_mem_iff; auto.
-Qed.
-
-Lemma add_fold: 
-  mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
-Proof.
-intros; apply add_fold with (eqA:=eqA); auto with set.
-Qed.
-
-Lemma remove_fold_1: 
- mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
-Proof.
-intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
-Qed.
-
-Lemma remove_fold_2: 
- mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
-Proof.
-intros; apply remove_fold_2 with (eqA:=eqA); auto.
-rewrite not_mem_iff; auto.
-Qed.
-
-Lemma fold_union: 
- (forall x, mem x s && mem x s'=false) -> 
- eqA (fold f (union s s') i) (fold f s (fold f s' i)).
-Proof.
-intros; apply fold_union with (eqA:=eqA); auto.
-intros; rewrite exclusive_set; auto.
-Qed.
-
-End Fold.
-
-(** Properties of [cardinal] *)
-
-Lemma add_cardinal_1: 
- forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
-Proof.
-auto with set.
-Qed.
-
-Lemma add_cardinal_2: 
- forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
-Proof.
-intros; apply add_cardinal_2; auto.
-rewrite not_mem_iff; auto.
-Qed.
-
-Lemma remove_cardinal_1: 
- forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
-Proof.
-intros; apply remove_cardinal_1; auto with set.
-Qed.
-
-Lemma remove_cardinal_2: 
- forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
-Proof.
-intros; apply Equal_cardinal; apply equal_2; auto with set.
-Qed.
-
-Lemma union_cardinal: 
- forall s s', (forall x, mem x s && mem x s'=false) -> 
- cardinal (union s s')=cardinal s+cardinal s'.
-Proof.
-intros; apply union_cardinal; auto; intros.
-rewrite exclusive_set; auto.
-Qed.
-
-Lemma subset_cardinal: 
- forall s s', subset s s'=true -> cardinal s<=cardinal s'.
-Proof.
-intros; apply subset_cardinal; auto with set.
-Qed.
-
-Section Bool.
-
-(** Properties of [filter] *)
-
-Variable f:elt->bool.
-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.
-Qed.
-
-Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
-Proof. 
-intros; apply filter_b; auto.
-Qed.
-
-Lemma for_all_filter: 
- forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
-Proof. 
-intros; apply bool_1; split; intros.
-apply is_empty_1.
-unfold Empty; intros. 
-rewrite filter_iff; auto.
-red; destruct 1.
-rewrite <- (@for_all_iff s f) in H; auto.
-rewrite (H a H0) in H1; discriminate.
-apply for_all_1; auto; red; intros.
-revert H; rewrite <- is_empty_iff.
-unfold Empty; intro H; generalize (H x); clear H.
-rewrite filter_iff; auto.
-destruct (f x); auto.
-Qed.
-
-Lemma exists_filter : 
- forall s, exists_ f s=negb (is_empty (filter f s)).
-Proof. 
-intros; apply bool_1; split; intros. 
-destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).
-apply bool_6.
-red; intros; apply (@is_empty_2 _ H0 a); auto with set.
-generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)).
-destruct (choose (filter f s)).
-intros H0 _; apply exists_1; auto.
-exists e; generalize (H0 e); rewrite filter_iff; auto.
-intros _ H0.
-rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate.
-Qed.
-
-Lemma partition_filter_1: 
- forall s, equal (fst (partition f s)) (filter f s)=true.
-Proof. 
-auto with set.
-Qed.
-
-Lemma partition_filter_2: 
- forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
-Proof. 
-auto with set.
-Qed.
-
-Lemma filter_add_1 : forall s x, f x = true -> 
- filter f (add x s) [=] add x (filter f s). 
-Proof.
-red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
-intuition.
-rewrite <- H; apply Comp; auto.
-Qed.
-
-Lemma filter_add_2 : forall s x, f x = false -> 
- filter f (add x s) [=] filter f s. 
-Proof.
-red; intros; do 2 (rewrite filter_iff; auto); set_iff.
-intuition.
-assert (f x = f a) by (apply Comp; auto).
-rewrite H in H1; rewrite H2 in H1; discriminate.
-Qed.
-
-Lemma add_filter_1 : forall s s' x, 
- f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
-Proof.
-unfold Add, MP.Add; intros.
-repeat rewrite filter_iff; auto.
-rewrite H0; clear H0.
-assert (E.eq x y -> f y = true) by 
- (intro H0; rewrite <- (Comp _ _ H0); auto).
-tauto.
-Qed.
-
-Lemma add_filter_2 : forall s s' x, 
- f x=false -> (Add x s s') -> filter f s [=] filter f s'.
-Proof.
-unfold Add, MP.Add, Equal; intros.
-repeat rewrite filter_iff; auto.
-rewrite H0; clear H0.
-assert (f a = true -> ~E.eq x a).
- intros H0 H1.
- rewrite (Comp _ _ H1) in H.
- rewrite H in H0; discriminate.
-tauto. 
-Qed.
-
-Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
-  forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
-Proof.
-clear Comp' Comp f.
-intros.
-assert (compat_bool E.eq (fun x => orb (f x) (g x))).
-  unfold compat_bool; 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).
-  split; auto with bool.
-  intro H3; destruct (orb_prop _ _ H3); auto.
-tauto.
-Qed.
-
-Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').
-Proof.
-unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.
-Qed.
-
-(** Properties of [for_all] *)
-
-Lemma for_all_mem_1: forall s, 
- (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
-Proof.
-intros.
-rewrite for_all_filter; auto.
-rewrite is_empty_equal_empty.
-apply equal_mem_1;intros.
-rewrite filter_b; auto.
-rewrite empty_mem.
-generalize (H a); case (mem a s);intros;auto.
-rewrite H0;auto.
-Qed.
-
-Lemma for_all_mem_2: forall s, 
- (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true. 
-Proof.
-intros.
-rewrite for_all_filter in H; auto.
-rewrite is_empty_equal_empty in H.
-generalize (equal_mem_2 _ _ H x).
-rewrite filter_b; auto.
-rewrite empty_mem.
-rewrite H0; simpl;intros.
-replace true with (negb false);auto;apply negb_sym;auto.
-Qed.
-
-Lemma for_all_mem_3: 
- forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
-Proof.
-intros.
-apply (bool_eq_ind (for_all f s));intros;auto.
-rewrite for_all_filter in H1; auto.
-rewrite is_empty_equal_empty in H1.
-generalize (equal_mem_2 _ _ H1 x).
-rewrite filter_b; auto.
-rewrite empty_mem.
-rewrite H.
-rewrite H0.
-simpl;auto.
-Qed.
-
-Lemma for_all_mem_4: 
- forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
-Proof.
-intros.
-rewrite for_all_filter in H; auto.
-destruct (choose_mem_3 _ H) as (x,(H0,H1));intros.
-exists x.
-rewrite filter_b in H1; auto.
-elim (andb_prop _ _ H1).
-split;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
-Qed.
-
-(** Properties of [exists] *)
-
-Lemma for_all_exists: 
- forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
-Proof.
-intros.
-rewrite for_all_b; auto.
-rewrite exists_b; auto.
-induction (elements s); simpl; auto.
-destruct (f a); simpl; auto.
-Qed.
-
-End Bool.
-Section Bool'.
-
-Variable f:elt->bool.
-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.
-Qed.
-
-Lemma exists_mem_1: 
- forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
-Proof.
-intros.
-rewrite for_all_exists; auto.
-rewrite for_all_mem_1;auto with bool.
-intros;generalize (H x H0);intros. 
-symmetry;apply negb_sym;simpl;auto.
-Qed.
-
-Lemma exists_mem_2: 
- forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false. 
-Proof.
-intros.
-rewrite for_all_exists in H; auto.
-replace false with (negb true);auto;apply negb_sym;symmetry.
-rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
-Qed.
-
-Lemma exists_mem_3: 
- forall s x, mem x s=true -> f x=true -> exists_ f s=true.
-Proof.
-intros.
-rewrite for_all_exists; auto.
-symmetry;apply negb_sym;simpl.
-apply for_all_mem_3 with x;auto.
-rewrite H0;auto.
-Qed.
-
-Lemma exists_mem_4: 
- forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
-Proof.
-intros.
-rewrite for_all_exists in H; auto.
-elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros.
-elim p;intros.
-exists x;split;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
-Qed.
-
-End Bool'.
-
-Section Sum.
-
-(** Adding a valuation function on all elements of a set. *)
-
-Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. 
-
-Lemma sum_plus : 
-  forall f g, compat_nat E.eq f -> compat_nat E.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_op E.eq (@eq _) (fun x:elt =>plus (f x))).  auto.
-assert (ft : transpose (@eq _) (fun x:elt =>plus (f x))). red; intros; omega.
-assert (gc : compat_op E.eq (@eq _) (fun x:elt => plus (g x))). auto.
-assert (gt : transpose (@eq _) (fun x:elt =>plus (g x))). red; intros; omega.
-assert (fgc : compat_op E.eq (@eq _) (fun x:elt =>plus ((f x)+(g x)))). auto.
-assert (fgt : transpose (@eq _) (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
-assert (st := gen_st nat).
-intros s;pattern s; apply set_rec.
-intros.
-rewrite <- (fold_equal _ _ st _ fc 0 _ _ H).
-rewrite <- (fold_equal _ _ st _ gc 0 _ _ H).
-rewrite <- (fold_equal _ _ st _ fgc 0 _ _ H); auto.
-intros; do 3 (rewrite (fold_add _ _ st);auto).
-rewrite H0;simpl;omega.
-intros; do 3 rewrite (fold_empty _ _ st);auto.
-Qed.
-
-Lemma sum_filter : forall f, (compat_bool E.eq f) -> 
-  forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
-Proof.
-unfold sum; intros f Hf.
-assert (st := gen_st nat).
-assert (cc : compat_op E.eq (@eq _) (fun x => plus (if f x then 1 else 0))). 
- unfold compat_op; intros.
- rewrite (Hf x x' H); auto.
-assert (ct : transpose (@eq _) (fun x => plus (if f x then 1 else 0))).
- unfold transpose; intros; omega.
-intros s;pattern s; apply set_rec.
-intros.
-change elt with E.t.
-rewrite <- (fold_equal _ _ st _ cc 0 _ _ H).
-rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto.
-intros; rewrite (fold_add _ _ st _ cc ct); auto.
-generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) .
-assert (~ In x (filter f s0)).
- intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H.
-case (f x); simpl; intros.
-rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto.
-rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto.
-intros; rewrite (fold_empty _ _ st);auto.
-rewrite MP.cardinal_1; auto.
-unfold Empty; intros.
-rewrite filter_iff; auto; set_iff; tauto.
-Qed.
-
-Lemma fold_compat : 
-  forall (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA))
-  (f g:elt->A->A),
-  (compat_op E.eq eqA f) -> (transpose eqA f) -> 
-  (compat_op E.eq eqA g) -> (transpose eqA g) -> 
-  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> 
-  (eqA (fold f s i) (fold g s i)).
-Proof.
-intros A eqA st f g fc ft gc gt i.
-intro s; pattern s; apply set_rec; intros.
-trans_st (fold f s0 i).
-apply fold_equal with (eqA:=eqA); auto.
-rewrite equal_sym; auto.
-trans_st (fold g s0 i).
-apply H0; intros; apply H1; auto with set.
-elim  (equal_2 H x); auto with set; intros.
-apply fold_equal with (eqA:=eqA); auto with set.
-trans_st (f x (fold f s0 i)).
-apply fold_add with (eqA:=eqA); auto with set.
-trans_st (g x (fold f s0 i)); auto with set.
-trans_st (g x (fold g s0 i)); auto with set.
-sym_st; apply fold_add with (eqA:=eqA); auto.
-trans_st i; [idtac | sym_st ]; apply fold_empty; auto.
-Qed.
-
-Lemma sum_compat : 
-  forall f g, compat_nat E.eq f -> compat_nat E.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 _ (@eq nat)); auto.
-unfold transpose; intros; omega.
-unfold transpose; intros; omega.
-Qed.
-
-End Sum.
-
-End EqProperties. 
+Module EqProperties (M:S).
+  Module D := OT_as_DT M.E.
+  Include FSetWeakEqProperties.EqProperties M D.
+End EqProperties.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index c2d69b9d24..dd24d29b4a 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -17,445 +17,32 @@
     [Equal s s'] instead of [equal s s'=true], etc. *)
 
 Require Export FSetInterface. 
-Require Import FSetFacts.
+Require Import DecidableTypeEx FSetFacts FSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 Hint Unfold transpose compat_op compat_nat.
 Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence.
 
-Module Properties (M: S).
-  Module ME:=OrderedTypeFacts(M.E).
-  Import ME. (* for ME.eq_dec *)
-  Import M.E.
-  Import M.
-  Module FM := Facts M.
-  Import FM.
-  Import Logic. (* to unmask [eq] *)  
-  Import Peano. (* to unmask [lt] *)
-
-  (** Results about lists without duplicates *)
-
-  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
-  Definition Above x s := forall y, In y s -> E.lt y x.
-  Definition Below x s := forall y, In y s -> E.lt x y.
-
-  Lemma In_dec : forall x s, {In x s} + {~ In x s}.
-  Proof.
-  intros; generalize (mem_iff s x); case (mem x s); intuition.
-  Qed.
-
-  Section BasicProperties.
-
-  (** properties of [Equal] *)
-
-  Lemma equal_refl : forall s, s[=]s.
-  Proof.
-  exact eq_refl.
-  Qed.
-
-  Lemma equal_sym : forall s s', s[=]s' -> s'[=]s.
-  Proof.
-  exact eq_sym.
-  Qed.
-
-  Lemma equal_trans : forall s1 s2 s3, s1[=]s2 -> s2[=]s3 -> s1[=]s3.
-  Proof.
-  exact eq_trans.
-  Qed.
-
-  Hint Immediate equal_refl equal_sym : set.
-
-  Variable s s' s'' s1 s2 s3 : t.
-  Variable x x' : elt.
-
-  (** properties of [Subset] *)
-  
-  Lemma subset_refl : s[<=]s. 
-  Proof.
-  apply Subset_refl.
-  Qed.
-
-  Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
-  Proof.
-  apply Subset_trans.
-  Qed.
-
-  Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
-  Proof.
-  unfold Subset, Equal; intuition.
-  Qed.
-
-  Hint Immediate subset_refl : set.
-
-  Lemma subset_equal : s[=]s' -> s[<=]s'.
-  Proof.
-  unfold Subset, Equal; intros; rewrite <- H; auto.
-  Qed.
-
-  Lemma subset_empty : empty[<=]s.
-  Proof.
-  unfold Subset; intros a; set_iff; intuition.
-  Qed.
-
-  Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2.
-  Proof.
-  unfold Subset; intros H a; set_iff; intuition.
-  Qed.
-
-  Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3.
-  Proof.
-  unfold Subset; intros H a; set_iff; intuition.
-  Qed.
-
-  Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2.
-  Proof.
-  unfold Subset; intros H H0 a; set_iff; intuition.
-  rewrite <- H2; auto.
-  Qed.
-
-  Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2.
-  Proof.
-  unfold Subset; intuition.
-  Qed.
-
-  Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.
-  Proof.
-  intros; rewrite <- H0; auto.
-  Qed.
- 
-  Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
-  Proof.
-  unfold Subset, Equal; split; intros; intuition; generalize (H a); intuition.
-  Qed.
-
-  (** properties of [empty] *)
-
-  Lemma empty_is_empty_1 : Empty s -> s[=]empty.
-  Proof.
-  unfold Empty, Equal; intros; generalize (H a); set_iff; tauto.
-  Qed.
-
-  Lemma empty_is_empty_2 : s[=]empty -> Empty s.
-  Proof.
-  unfold Empty, Equal; intros; generalize (H a); set_iff; tauto.
-  Qed.
-
-  (** properties of [add] *)
-
-  Lemma add_equal : In x s -> add x s [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  rewrite <- H1; auto.
-  Qed.
- 
-  Lemma add_add : add x (add x' s) [=] add x' (add x s).
-  Proof. 
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  (** properties of [remove] *)
-
-  Lemma remove_equal : ~ In x s -> remove x s [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  rewrite H1 in H; auto.
-  Qed.
-
-  Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
-
-  (** properties of [add] and [remove] *)
-
-  Lemma add_remove : In x s -> add x (remove x s) [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; elim (eq_dec x a); intuition.
-  rewrite <- H1; auto.
-  Qed.
-
-  Lemma remove_add : ~In x s -> remove x (add x s) [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; elim (eq_dec x a); intuition.
-  rewrite H1 in H; auto.
-  Qed.
-
-  (** properties of [singleton] *)
-
-  Lemma singleton_equal_add : singleton x [=] add x empty.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  Qed.
-
-  (** properties of [union] *)
-
-  Lemma union_sym : union s s' [=] union s' s.
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'.
-  Proof.
-  unfold Subset, Equal; intros; set_iff; intuition.
-  Qed.
-
-  Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
-
-  Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
-
-  Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  Lemma add_union_singleton : add x s [=] union (singleton x) s.
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  Lemma union_add : union (add x s) s' [=] add x (union s s').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  Lemma union_remove_add_1 : 
-   union (remove x s) (add x s') [=] union (add x s) (remove x s').
-  Proof.
-  unfold Equal; intros; set_iff.
-  destruct (eq_dec x a); intuition.
-  Qed.
-
-  Lemma union_remove_add_2 : In x s -> 
-   union (remove x s) (add x s') [=] union s s'.
-  Proof.
-  unfold Equal; intros; set_iff.
-  destruct (eq_dec x a); intuition.
-  left; eauto with set.
-  Qed.
-
-  Lemma union_subset_1 : s [<=] union s s'.
-  Proof.
-  unfold Subset; intuition.
-  Qed.
-
-  Lemma union_subset_2 : s' [<=] union s s'.
-  Proof.
-  unfold Subset; intuition.
-  Qed.
-
-  Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''.
-  Proof.
-  unfold Subset; intros H H0 a; set_iff; intuition.
-  Qed.
-
-  Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.
-  Proof. 
-  unfold Subset; intros H a; set_iff; intuition.
-  Qed.
-
-  Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.
-  Proof. 
-  unfold Subset; intros H a; set_iff; intuition.
-  Qed.
-
-  Lemma empty_union_1 : Empty s -> union s s' [=] s'.
-  Proof.
-  unfold Equal, Empty; intros; set_iff; firstorder.
-  Qed.
-
-  Lemma empty_union_2 : Empty s -> union s' s [=] s'.
-  Proof.
-  unfold Equal, Empty; intros; set_iff; firstorder.
-  Qed.
-
-  Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s'). 
-  Proof.
-  intros; set_iff; intuition. 
-  Qed.  
-
-  (** properties of [inter] *)
-
-  Lemma inter_sym : inter s s' [=] inter s' s.
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  Qed.
+(** First, the properties that do not rely on the element ordering 
+    are imported verbatim from FSetWeakProperties *)
 
-  Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
-
-  Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
-
-  Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s'').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s'').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s').
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  rewrite <- H1; auto.
-  Qed.
-
-  Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  destruct H; rewrite H0; auto.
-  Qed.
-
-  Lemma empty_inter_1 : Empty s -> Empty (inter s s').
-  Proof.
-  unfold Empty; intros; set_iff; firstorder.
-  Qed.
-
-  Lemma empty_inter_2 : Empty s' -> Empty (inter s s').
-  Proof.
-  unfold Empty; intros; set_iff; firstorder.
-  Qed.
-
-  Lemma inter_subset_1 : inter s s' [<=] s.
-  Proof.
-  unfold Subset; intro a; set_iff; tauto.
-  Qed.
-
-  Lemma inter_subset_2 : inter s s' [<=] s'.
-  Proof.
-  unfold Subset; intro a; set_iff; tauto.
-  Qed.
-
-  Lemma inter_subset_3 :
-   s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'.
-  Proof.
-  unfold Subset; intros H H' a; set_iff; intuition.
-  Qed.
-
-  (** properties of [diff] *)
-
-  Lemma empty_diff_1 : Empty s -> Empty (diff s s'). 
-  Proof.
-  unfold Empty, Equal; intros; set_iff; firstorder.
-  Qed.
-
-  Lemma empty_diff_2 : Empty s -> diff s' s [=] s'.
-  Proof.
-  unfold Empty, Equal; intros; set_iff; firstorder.
-  Qed.
-
-  Lemma diff_subset : diff s s' [<=] s.
-  Proof.
-  unfold Subset; intros a; set_iff; tauto.
-  Qed.
-
-  Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty.
-  Proof.
-  unfold Subset, Equal; intros; set_iff; intuition; absurd (In a empty); auto.
-  Qed.
+Require FSetWeakProperties.
 
-  Lemma remove_diff_singleton :
-   remove x s [=] diff s (singleton x).
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  Qed.
-
-  Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty. 
-  Proof.
-  unfold Equal; intros; set_iff; intuition; absurd (In a empty); auto.
-  Qed.
-
-  Lemma diff_inter_all : union (diff s s') (inter s s') [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  elim (In_dec a s'); auto.
-  Qed.
-
-  (** properties of [Add] *)
-
-  Lemma Add_add : Add x s (add x s).
-  Proof.
-   unfold Add; intros; set_iff; intuition.
-  Qed.
-
-  Lemma Add_remove : In x s -> Add x (remove x s) s. 
-  Proof. 
-    unfold Add; intros; set_iff; intuition.
-    elim (eq_dec x y); auto.
-    rewrite <- H1; auto.
-  Qed.
-
-  Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s'').
-  Proof. 
-  unfold Add; intros; set_iff; rewrite H; tauto.
-  Qed.
-
-  Lemma inter_Add :
-   In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'').
-  Proof. 
-  unfold Add; intros; set_iff; rewrite H0; intuition.
-  rewrite <- H2; auto.
-  Qed.  
-
-  Lemma union_Equal :
-   In x s'' -> Add x s s' -> union s s'' [=] union s' s''.
-  Proof. 
-  unfold Add, Equal; intros; set_iff; rewrite H0; intuition. 
-  rewrite <- H1; auto.
-  Qed.  
-
-  Lemma inter_Add_2 :
-   ~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''.
-  Proof.
-  unfold Add, Equal; intros; set_iff; rewrite H0; intuition.
-  destruct H; rewrite H1; auto.
-  Qed.
-
-  End BasicProperties.
-
-  Hint Immediate equal_sym: set.
-  Hint Resolve equal_refl equal_trans : set.
-
-  Hint Immediate add_remove remove_add union_sym inter_sym: set.
-  Hint Resolve subset_refl subset_equal subset_antisym 
-    subset_trans subset_empty subset_remove_3 subset_diff subset_add_3 
-    subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
-    remove_equal singleton_equal_add union_subset_equal union_equal_1 
-    union_equal_2 union_assoc add_union_singleton union_add union_subset_1 
-    union_subset_2 union_subset_3 inter_subset_equal inter_equal_1 inter_equal_2
-    inter_assoc union_inter_1 union_inter_2 inter_add_1 inter_add_2
-    empty_inter_1 empty_inter_2 empty_union_1 empty_union_2 empty_diff_1 
-    empty_diff_2 union_Add inter_Add union_Equal inter_Add_2 not_in_union 
-    inter_subset_1 inter_subset_2 inter_subset_3 diff_subset diff_subset_equal 
-    remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
-    Equal_remove add_add : set.
+Module Properties (M:S).
+  Module D := OT_as_DT M.E.
+  Include FSetWeakProperties.Properties M D.
+End Properties.
 
-  (** * Properties of elements *)
+(** Now comes some properties specific to the element ordering, 
+    invalid in FSetWeak. *)
 
-  Section Elements.
+Module OrdProperties (M:S).
+  Module ME:=OrderedTypeFacts(M.E).
+  Module Import P := Properties M.
+  Import FM.
+  Import M.E.
+  Import M.
 
   (* First, a specialized version of SortA_equivlistA_eqlistA: *)
   Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
@@ -464,24 +51,6 @@ Module Properties (M: S).
   apply SortA_equivlistA_eqlistA; eauto.
   Qed.
 
-  Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
-  Proof.
-  intros.
-  unfold Empty.
-  split; intros.
-  assert (forall a, ~ List.In a (elements s)).
-   red; intros.
-   apply (H a).
-   rewrite elements_iff.
-   rewrite InA_alt; exists a; auto.
-  destruct (elements s); auto.
-  elim (H0 e); simpl; auto.
-  red; intros.
-  rewrite elements_iff in H0.
-  rewrite InA_alt in H0; destruct H0.
-  rewrite H in H0; destruct H0 as (_,H0); inversion H0.
-  Qed.
-
   Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
   Definition leb x := fun y => negb (gtb x y).
 
@@ -540,7 +109,7 @@ Module Properties (M: S).
   apply (@filter_sort _ E.eq); auto with set; eauto with set.
   constructor; auto.
   apply (@filter_sort _ E.eq); auto with set; eauto with set.
-  rewrite Inf_alt; auto; intros.
+  rewrite ME.Inf_alt; auto; intros.
   apply (@filter_sort _ E.eq); auto with set; eauto with set.
   rewrite filter_InA in H1; auto; destruct H1.
   rewrite leb_1 in H2.
@@ -567,6 +136,9 @@ Module Properties (M: S).
   ME.order.
   Qed.
 
+  Definition Above x s := forall y, In y s -> E.lt y x.
+  Definition Below x s := forall y, In y s -> E.lt x y.
+
   Lemma elements_Add_Above : forall s s' x, 
    Above x s -> Add x s s' -> 
      eqlistA E.eq (elements s') (elements s ++ x::nil).
@@ -577,7 +149,7 @@ Module Properties (M: S).
   intros.
   inversion_clear H2.
   rewrite <- elements_iff in H1.
-  apply lt_eq with x; auto.
+  apply ME.lt_eq with x; auto.
   inversion H3.
   red; intros a.
   rewrite InA_app_iff; rewrite InA_cons; rewrite InA_nil.
@@ -595,109 +167,13 @@ Module Properties (M: S).
   intros.
   inversion_clear H1.
   rewrite <- elements_iff in H2.
-  apply eq_lt with x; auto.
+  apply ME.eq_lt with x; auto.
   inversion H3.
   red; intros a.
   rewrite InA_cons.
   do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
   Qed.
 
-  End Elements.
-
-  (** * Properties of cardinal (proved using [elements]) *)
-
-  Section Cardinal.
-
-  Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
-  Proof.
-  intros.
-  do 2 rewrite M.cardinal_1.
-  apply (@eqlistA_length _ E.eq); auto.
-  apply sort_equivlistA_eqlistA; auto with set.
-  red; intro a.
-  do 2 rewrite <- elements_iff; auto.
-  Qed.
-
-  Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
-  Proof.
-   intros.
-   rewrite elements_Empty.
-   rewrite cardinal_1.
-   destruct (elements s); intuition; discriminate.
-  Qed.
-
-  Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s. 
-  Proof. 
-    intros. rewrite cardinal_Empty; auto.
-  Qed.
-
-  Lemma cardinal_inv_2 :
-   forall s n, cardinal s = S n -> { x : elt | In x s }.
-  Proof. 
-    intros; rewrite M.cardinal_1 in H.
-    generalize (elements_2 (s:=s)).
-    destruct (elements s); try discriminate. 
-    exists e; auto.
-  Qed.
-
-  Lemma cardinal_inv_2b :
-   forall s, cardinal s <> 0 -> { x : elt | In x s }.
-  Proof.
-    intros; rewrite M.cardinal_1 in H.
-    generalize (elements_2 (s:=s)).
-    destruct (elements s); simpl in H.
-    elim H; auto.
-    exists e; auto.
-  Qed.
-
-  Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
-  Proof.
-    intros. rewrite <- cardinal_Empty; auto.
-  Qed.
-
-  Lemma cardinal_2 : forall s s' x, ~In x s -> Add x s s' -> 
-    cardinal s' = S (cardinal s).
-  Proof.
-  intros.
-  do 2 rewrite M.cardinal_1.
-  unfold elt.
-  rewrite (eqlistA_length (elements_Add H H0)); simpl.
-  rewrite app_length; simpl.
-  rewrite <- plus_n_Sm.
-  f_equal.
-  rewrite <- app_length.
-  f_equal.
-  symmetry; apply elements_split; auto.
-  Qed.
-
-  End Cardinal.
-
-  Add Morphism cardinal : cardinal_m.
-  Proof.
-  exact Equal_cardinal.
-  Qed.
-
-  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
-
-  (** * Induction principle over sets *)
-
-  Section Induction_Principles.
-
-  Lemma set_induction :
-   forall P : t -> Type,
-   (forall s : t, Empty s -> P s) ->
-   (forall s s' : t, P s -> forall x : elt, ~In x s -> Add x s s' -> P s') ->
-   forall s : t, P s.
-  Proof.
-  intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
-  destruct (cardinal_inv_2 (sym_eq Heqn)) as (x,H0). 
-  apply X0 with (remove x s) x; auto with set.
-  apply IHn; auto.
-  assert (S n = S (cardinal (remove x s))).
-    rewrite Heqn; apply cardinal_2 with x; auto with set.
-  inversion H; auto.
-  Qed.
-
   (** Two other induction principles on sets: we can be more restrictive 
       on the element we add at each step.  *)
 
@@ -720,7 +196,7 @@ Module Properties (M: S).
 
   assert (H0:=max_elt_3 H).
   rewrite cardinal_Empty in H0; rewrite H0 in Heqn; inversion Heqn.
-  Qed.  
+  Qed.
 
   Lemma set_induction_min :
    forall P : t -> Type,
@@ -733,7 +209,7 @@ Module Properties (M: S).
   apply X0 with (remove e s) e; auto with set.
   apply IHn.
   assert (S n = S (cardinal (remove e s))).
-   rewrite Heqn; apply cardinal_2 with e; auto with set. 
+   rewrite Heqn; apply cardinal_2 with e; auto with set.
   inversion H0; auto.
   red; intros.
   rewrite remove_iff in H0; destruct H0.
@@ -743,69 +219,7 @@ Module Properties (M: S).
   rewrite cardinal_Empty in H0; auto; rewrite H0 in Heqn; inversion Heqn.
   Qed.
 
-  End Induction_Principles.
-
-  Section Fold_Basic. 
-
-  Notation NoDup := (NoDupA E.eq).
- 
-  (** * Alternative (weaker) specifications for [fold] *)
-
-  (** When [FSets] was first designed, the order in which Ocaml's [Set.fold]
-        takes the set elements was unspecified. This specification reflects this fact: 
-  *)
-
-  Lemma fold_0 : 
-      forall s (A : Type) (i : A) (f : elt -> A -> A),
-      exists l : list elt,
-        NoDup l /\
-        (forall x : elt, In x s <-> InA E.eq x l) /\
-        fold f s i = fold_right f i l.
-  Proof.
-  intros; exists (rev (elements s)); split.
-  apply NoDupA_rev; auto with set.
-  exact E.eq_trans.
-  split; intros.
-  rewrite elements_iff; do 2 rewrite InA_alt.
-  split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
-  rewrite fold_left_rev_right.
-  apply fold_1.
-  Qed.
-
-  (** An alternate (and previous) specification for [fold] was based on 
-      the recursive structure of a set. It is now lemmas [fold_1] and 
-      [fold_2]. *)
-
-  Lemma fold_1 :
-   forall s (A : Set) (eqA : A -> A -> Prop) 
-     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
-   Empty s -> eqA (fold f s i) i.
-  Proof.
-  intros; rewrite M.fold_1.
-  rewrite elements_Empty in H; rewrite H.
-  simpl; refl_st.
-  Qed.
-
-  Lemma fold_2 :
-   forall s s' x (A : Set) (eqA : A -> A -> Prop)
-     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
-   compat_op E.eq eqA f ->
-   transpose eqA f ->
-   ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
-  Proof.
-  intros; do 2 rewrite M.fold_1; do 2 rewrite <- fold_left_rev_right.
-  trans_st (fold_right f i (rev (elements_lt x s ++ x :: elements_ge x s))).
-  apply fold_right_eqlistA with (eqA:=E.eq) (eqB:=eqA); auto.
-  apply eqlistA_rev.
-  apply elements_Add; auto.
-  rewrite distr_rev; simpl.
-  rewrite app_ass; simpl.
-  rewrite (elements_split x s).
-  rewrite distr_rev; simpl.
-  apply fold_right_commutes with (eqA:=E.eq) (eqB:=eqA); auto.
-  Qed.
-
-  (** More properties of [fold] : behavior with respect to Above/Below *) 
+  (** More properties of [fold] : behavior with respect to Above/Below *)
 
   Lemma fold_3 :
    forall s s' x (A : Set) (eqA : A -> A -> Prop)
@@ -816,7 +230,7 @@ Module Properties (M: S).
   intros.
   do 2 rewrite M.fold_1.
   do 2 rewrite <- fold_left_rev_right.
-  change (f x (fold_right f i (rev (elements s)))) with 
+  change (f x (fold_right f i (rev (elements s)))) with
     (fold_right f i (rev (x::nil)++rev (elements s))).
   apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
   rewrite <- distr_rev.
@@ -841,18 +255,13 @@ Module Properties (M: S).
   apply elements_Add_Below; auto.
   Qed.
 
-  End Fold_Basic.
-
-  (** Other properties of [fold]. *)
+  (** The following results have already been proved earlier, 
+    but we can now prove them with one hypothesis less:
+    no need for [(transpose eqA f)]. *)
 
-  Section Fold_More. 
+  Section FoldOpt. 
   Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
-  Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
-
-  Lemma fold_empty : forall i, eqA (fold f empty i) i.
-  Proof. 
-  intros; apply fold_1; auto with set.
-  Qed.
+  Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f).
 
   Lemma fold_equal : 
    forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
@@ -873,26 +282,12 @@ Module Properties (M: S).
   induction (rev (elements s)); simpl; auto.
   Qed.
 
-  Lemma fold_add : forall i s x, ~In x s -> 
-   eqA (fold f (add x s) i) (f x (fold f s i)).
-  Proof. 
-  intros; apply fold_2 with (eqA := eqA); auto.
-  Qed.
-
   Lemma add_fold : forall i s x, In x s -> 
    eqA (fold f (add x s) i) (fold f s i).
   Proof.
   intros; apply fold_equal; auto with set.
   Qed.
 
-  Lemma remove_fold_1: forall i s x, In x s -> 
-   eqA (f x (fold f (remove x s) i)) (fold f s i).
-  Proof.
-  intros.
-  sym_st.
-  apply fold_2 with (eqA:=eqA); auto with set.
-  Qed.
-
   Lemma remove_fold_2: forall i s x, ~In x s -> 
    eqA (fold f (remove x s) i) (fold f s i).
   Proof.
@@ -900,210 +295,6 @@ Module Properties (M: S).
   apply fold_equal; auto with set.
   Qed.
 
-  Lemma fold_commutes : forall i s x, 
-   eqA (fold f s (f x i)) (f x (fold f s i)).
-  Proof.
-  intros; do 2 rewrite M.fold_1.
-  do 2 rewrite <- fold_left_rev_right.
-  induction (rev (elements s)); simpl; auto.
-  refl_st.
-  trans_st (f a (f x (fold_right f i l))).
-  Qed.
-
-  Lemma fold_union_inter : forall i s s',
-   eqA (fold f (union s s') (fold f (inter s s') i))
-       (fold f s (fold f s' i)).
-  Proof.
-  intros; pattern s; apply set_induction; clear s; intros.
-  trans_st (fold f s' (fold f (inter s s') i)).
-  apply fold_equal; auto with set.
-  trans_st (fold f s' i).
-  apply fold_init; auto.
-  apply fold_1; auto with set.
-  sym_st; apply fold_1; auto.
-  rename s'0 into s''.
-  destruct (In_dec x s').
-  (* In x s' *)   
-  trans_st (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set.
-  apply fold_init; auto.
-  apply fold_2 with (eqA:=eqA); auto with set.
-  rewrite inter_iff; intuition.
-  trans_st (f x (fold f s (fold f s' i))).
-  trans_st (fold f (union s s') (f x (fold f (inter s s') i))).
-  apply fold_equal; auto.
-  apply equal_sym; apply union_Equal with x; auto with set.
-  trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
-  apply fold_commutes; auto.
-  sym_st; apply fold_2 with (eqA:=eqA); auto.
-  (* ~(In x s') *)
-  trans_st (f x (fold f (union s s') (fold f (inter s'' s') i))).
-  apply fold_2 with (eqA:=eqA); auto with set.
-  trans_st (f x (fold f (union s s') (fold f (inter s s') i))).
-  apply Comp;auto.
-  apply fold_init;auto.
-  apply fold_equal;auto.
-  apply equal_sym; apply inter_Add_2 with x; auto with set.
-  trans_st (f x (fold f s (fold f s' i))).
-  sym_st; apply fold_2 with (eqA:=eqA); auto.
-  Qed.
-
-  Lemma fold_diff_inter : forall i s s', 
-   eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i).
-  Proof.
-  intros.
-  trans_st (fold f (union (diff s s') (inter s s')) 
-              (fold f (inter (diff s s') (inter s s')) i)).
-  sym_st; apply fold_union_inter; auto.
-  trans_st (fold f s (fold f (inter (diff s s') (inter s s')) i)).
-  apply fold_equal; auto with set.
-  apply fold_init; auto.
-  apply fold_1; auto with set.
-  Qed.
-
-  Lemma fold_union: forall i s s', 
-   (forall x, ~(In x s/\In x s')) ->
-   eqA (fold f (union s s') i) (fold f s (fold f s' i)).
-  Proof.
-  intros.
-  trans_st (fold f (union s s') (fold f (inter s s') i)).
-  apply fold_init; auto.
-  sym_st; apply fold_1; auto with set.
-  unfold Empty; intro a; generalize (H a); set_iff; tauto.
-  apply fold_union_inter; auto.
-  Qed.
-
-  End Fold_More.
-
-  Lemma fold_plus :
-   forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
-  Proof.
-  intros; do 2 rewrite M.fold_1.
-  do 2 rewrite <- fold_left_rev_right.
-  induction (rev (elements s)); simpl; auto.
-  Qed.
-
-  (** more properties of [cardinal] *)
-
-  Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
-  Proof.
-  intros; rewrite M.cardinal_1; rewrite M.fold_1.
-  symmetry; apply fold_left_length; auto.
-  Qed.
-
-  Lemma empty_cardinal : cardinal empty = 0.
-  Proof.
-  rewrite cardinal_fold; apply fold_1; auto with set.
-  Qed.
-
-  Hint Immediate empty_cardinal cardinal_1 : set.
-
-  Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
-  Proof.
-  intros.
-  rewrite (singleton_equal_add x).
-  replace 0 with (cardinal empty); auto with set.
-  apply cardinal_2 with x; auto with set.
-  Qed.
-
-  Hint Resolve singleton_cardinal: set.
-
-  Lemma diff_inter_cardinal :
-   forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s .
-  Proof.
-  intros; do 3 rewrite cardinal_fold.
-  rewrite <- fold_plus.
-  apply fold_diff_inter with (eqA:=@eq nat); auto.
-  Qed.
-
-  Lemma union_cardinal: 
-   forall s s', (forall x, ~(In x s/\In x s')) -> 
-   cardinal (union s s')=cardinal s+cardinal s'.
-  Proof.
-  intros; do 3 rewrite cardinal_fold.
-  rewrite <- fold_plus.
-  apply fold_union; auto.
-  Qed.
-
-  Lemma subset_cardinal : 
-   forall s s', s[<=]s' -> cardinal s <= cardinal s' .
-  Proof.
-  intros.
-  rewrite <- (diff_inter_cardinal s' s).
-  rewrite (inter_sym s' s).
-  rewrite (inter_subset_equal H); auto with arith.
-  Qed.
-
-  Lemma subset_cardinal_lt : 
-   forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.
-  Proof. 
-  intros.
-  rewrite <- (diff_inter_cardinal s' s).
-  rewrite (inter_sym s' s).
-  rewrite (inter_subset_equal H).
-  generalize (@cardinal_inv_1 (diff s' s)).
-  destruct (cardinal (diff s' s)).
-  intro H2; destruct (H2 (refl_equal _) x).
-  set_iff; auto.
-  intros _.
-  change (0 + cardinal s < S n + cardinal s).
-  apply Plus.plus_lt_le_compat; auto with arith.
-  Qed. 
-
-  Theorem union_inter_cardinal :
-   forall s s', cardinal (union s s') + cardinal (inter s s')  = cardinal s  + cardinal s' .
-  Proof.
-  intros.
-  do 4 rewrite cardinal_fold.
-  do 2 rewrite <- fold_plus.
-  apply fold_union_inter with (eqA:=@eq nat); auto.
-  Qed.
-
-  Lemma union_cardinal_inter : 
-   forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s').
-  Proof.
-  intros.
-  rewrite <- union_inter_cardinal.
-  rewrite Plus.plus_comm.
-  auto with arith.
-  Qed.
-
-  Lemma union_cardinal_le : 
-   forall s s', cardinal (union s s') <= cardinal s  + cardinal s'.
-  Proof.
-   intros; generalize (union_inter_cardinal s s').
-   intros; rewrite <- H; auto with arith.
-  Qed.
-
-  Lemma add_cardinal_1 : 
-   forall s x, In x s -> cardinal (add x s) = cardinal s.
-  Proof.
-  auto with set.  
-  Qed.
-
-  Lemma add_cardinal_2 :
-   forall s x, ~In x s -> cardinal (add x s) = S (cardinal s).
-  Proof.
-  intros.
-  do 2 rewrite cardinal_fold.
-  change S with ((fun _ => S) x);
-   apply fold_add with (eqA:=@eq nat); auto.
-  Qed.
-
-  Lemma remove_cardinal_1 :
-   forall s x, In x s -> S (cardinal (remove x s)) = cardinal s.
-  Proof.
-  intros.
-  do 2 rewrite cardinal_fold.
-  change S with ((fun _ =>S) x).
-  apply remove_fold_1 with (eqA:=@eq nat); auto.
-  Qed.
-
-  Lemma remove_cardinal_2 : 
-   forall s x, ~In x s -> cardinal (remove x s) = cardinal s.
-  Proof. 
-  auto with set.
-  Qed.
-
-  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
+  End FoldOpt.
 
-End Properties.
+End OrdProperties.
diff --git a/theories/FSets/FSetWeakEqProperties.v b/theories/FSets/FSetWeakEqProperties.v
new file mode 100644
index 0000000000..d5fa13bddc
--- /dev/null
+++ b/theories/FSets/FSetWeakEqProperties.v
@@ -0,0 +1,934 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(** * Finite sets library *)
+
+(** This module proves many properties of finite sets that 
+    are consequences of the axiomatization in [FsetInterface] 
+    Contrary to the functor in [FsetWeakProperties] it uses 
+    sets operations instead of predicates over sets, i.e.
+    [mem x s=true] instead of [In x s], 
+    [equal s s'=true] instead of [Equal s s'], etc. *)
+
+Require Import FSetWeakProperties Zerob Sumbool Omega.
+
+Module EqProperties 
+ (M:S)
+ (D:DecidableType with Definition t:=M.E.t
+                  with Definition eq:=M.E.eq).
+Module Import MP := Properties M D.
+Import FM.
+Import M.E.
+Import M.
+
+Definition Add := MP.Add.
+
+Section BasicProperties. 
+
+(** Some old specifications written with boolean equalities. *) 
+
+Variable s s' s'': t.
+Variable x y z : elt.
+
+Lemma mem_eq: 
+  E.eq x y -> mem x s=mem y s.
+Proof. 
+intro H; rewrite H; auto.
+Qed.
+
+Lemma equal_mem_1: 
+  (forall a, mem a s=mem a s') -> equal s s'=true.
+Proof. 
+intros; apply equal_1; unfold Equal; intros.
+do 2 rewrite mem_iff; rewrite H; tauto.
+Qed.
+
+Lemma equal_mem_2: 
+  equal s s'=true -> forall a, mem a s=mem a s'.
+Proof. 
+intros; rewrite (equal_2 H); auto.
+Qed.
+
+Lemma subset_mem_1: 
+  (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
+Proof. 
+intros; apply subset_1; unfold Subset; intros a.
+do 2 rewrite mem_iff; auto.
+Qed.
+
+Lemma subset_mem_2: 
+  subset s s'=true -> forall a, mem a s=true -> mem a s'=true.
+Proof. 
+intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
+Qed.
+  
+Lemma empty_mem: mem x empty=false.
+Proof. 
+rewrite <- not_mem_iff; auto with set.
+Qed.
+
+Lemma is_empty_equal_empty: is_empty s = equal s empty.
+Proof. 
+apply bool_1; split; intros.
+rewrite <- (empty_is_empty_1 (s:=empty)); auto with set.
+rewrite <- is_empty_iff; auto with set.
+Qed.
+  
+Lemma choose_mem_1: choose s=Some x -> mem x s=true.
+Proof.  
+auto with set.
+Qed.
+
+Lemma choose_mem_2: choose s=None -> is_empty s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_mem_1: mem x (add x s)=true.
+Proof.
+auto with set.
+Qed.  
+ 
+Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
+Proof. 
+apply add_neq_b.
+Qed.
+
+Lemma remove_mem_1: mem x (remove x s)=false.
+Proof. 
+rewrite <- not_mem_iff; auto with set.
+Qed. 
+ 
+Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
+Proof. 
+apply remove_neq_b.
+Qed.
+
+Lemma singleton_equal_add: 
+  equal (singleton x) (add x empty)=true.
+Proof.
+rewrite (singleton_equal_add x); auto with set.
+Qed.  
+
+Lemma union_mem: 
+  mem x (union s s')=mem x s || mem x s'.
+Proof. 
+apply union_b.
+Qed.
+
+Lemma inter_mem: 
+  mem x (inter s s')=mem x s && mem x s'.
+Proof. 
+apply inter_b.
+Qed.
+
+Lemma diff_mem: 
+  mem x (diff s s')=mem x s && negb (mem x s').
+Proof. 
+apply diff_b.
+Qed.
+
+(** properties of [mem] *)
+
+Lemma mem_3 : ~In x s -> mem x s=false.
+Proof.
+intros; rewrite <- not_mem_iff; auto.
+Qed.
+
+Lemma mem_4 : mem x s=false -> ~In x s.
+Proof.
+intros; rewrite not_mem_iff; auto.
+Qed.
+
+(** Properties of [equal] *) 
+
+Lemma equal_refl: equal s s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma equal_sym: equal s s'=equal s' s.
+Proof.
+intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
+Qed.
+
+Lemma equal_trans: 
+ equal s s'=true -> equal s' s''=true -> equal s s''=true.
+Proof.
+intros; rewrite (equal_2 H); auto.
+Qed.
+
+Lemma equal_equal: 
+ equal s s'=true -> equal s s''=equal s' s''.
+Proof.
+intros; rewrite (equal_2 H); auto.
+Qed.
+
+Lemma equal_cardinal: 
+ equal s s'=true -> cardinal s=cardinal s'.
+Proof.
+auto with set.
+Qed.
+
+(* Properties of [subset] *)
+
+Lemma subset_refl: subset s s=true. 
+Proof.
+auto with set.
+Qed.
+
+Lemma subset_antisym: 
+ subset s s'=true -> subset s' s=true -> equal s s'=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma subset_trans: 
+ subset s s'=true -> subset s' s''=true -> subset s s''=true.
+Proof.
+do 3 rewrite <- subset_iff; intros.
+apply subset_trans with s'; auto.
+Qed.
+
+Lemma subset_equal: 
+ equal s s'=true -> subset s s'=true.
+Proof.
+auto with set.
+Qed.
+
+(** Properties of [choose] *)
+
+Lemma choose_mem_3: 
+ is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
+Proof.
+intros.
+generalize (@choose_1 s) (@choose_2 s).
+destruct (choose s);intros.
+exists e;auto with set.
+generalize (H1 (refl_equal None)); clear H1.
+intros; rewrite (is_empty_1 H1) in H; discriminate.
+Qed.
+
+Lemma choose_mem_4: choose empty=None.
+Proof.
+generalize (@choose_1 empty).
+case (@choose empty);intros;auto.
+elim (@empty_1 e); auto.
+Qed.
+
+(** Properties of [add] *)
+
+Lemma add_mem_3: 
+ mem y s=true -> mem y (add x s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_equal: 
+ mem x s=true -> equal (add x s) s=true.
+Proof.
+auto with set.
+Qed.
+
+(** Properties of [remove] *)
+
+Lemma remove_mem_3: 
+ mem y (remove x s)=true -> mem y s=true.
+Proof.
+rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
+Qed.
+
+Lemma remove_equal: 
+ mem x s=false -> equal (remove x s) s=true.
+Proof.
+intros; apply equal_1; apply remove_equal.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma add_remove: 
+ mem x s=true -> equal (add x (remove x s)) s=true.
+Proof.
+intros; apply equal_1; apply add_remove; auto with set.
+Qed.
+
+Lemma remove_add: 
+ mem x s=false -> equal (remove x (add x s)) s=true.
+Proof.
+intros; apply equal_1; apply remove_add; auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+(** Properties of [is_empty] *)
+
+Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
+Proof.
+intros; apply bool_1; split; intros.
+rewrite MP.cardinal_1; simpl; auto with set.
+assert (cardinal s = 0) by (apply zerob_true_elim; auto).
+auto with set.
+Qed.
+
+(** Properties of [singleton] *)
+
+Lemma singleton_mem_1: mem x (singleton x)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
+Proof.
+intros; rewrite singleton_b.
+unfold eqb; destruct (eq_dec x y); intuition.
+Qed.
+
+Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
+Proof.
+intros; apply singleton_1; auto with set.
+Qed.
+
+(** Properties of [union] *)
+
+Lemma union_sym:
+ equal (union s s') (union s' s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_subset_equal: 
+ subset s s'=true -> equal (union s s') s'=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_equal_1: 
+ equal s s'=true-> equal (union s s'') (union s' s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_equal_2: 
+ equal s' s''=true-> equal (union s s') (union s s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_assoc: 
+ equal (union (union s s') s'') (union s (union s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_union_singleton: 
+ equal (add x s) (union (singleton x) s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_add: 
+ equal (union (add x s) s') (add x (union s s'))=true.
+Proof.
+auto with set.
+Qed.
+
+(* caracterisation of [union] via [subset] *)
+
+Lemma union_subset_1: subset s (union s s')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_subset_2: subset s' (union s s')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_subset_3:
+ subset s s''=true -> subset s' s''=true -> 
+  subset (union s s') s''=true.
+Proof.
+intros; apply subset_1; apply union_subset_3; auto with set.
+Qed.
+
+(** Properties of [inter] *) 
+
+Lemma inter_sym: equal (inter s s') (inter s' s)=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_subset_equal: 
+ subset s s'=true -> equal (inter s s') s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_equal_1: 
+ equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_equal_2: 
+ equal s' s''=true -> equal (inter s s') (inter s s'')=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_assoc: 
+ equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_inter_1: 
+ equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma union_inter_2: 
+ equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_add_1: mem x s'=true -> 
+ equal (inter (add x s) s') (add x (inter s s'))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_add_2: mem x s'=false -> 
+ equal (inter (add x s) s') (inter s s')=true.
+Proof.
+intros; apply equal_1; apply inter_add_2.
+rewrite not_mem_iff; auto.
+Qed.
+
+(* caracterisation of [union] via [subset] *)
+
+Lemma inter_subset_1: subset (inter s s') s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_subset_2: subset (inter s s') s'=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma inter_subset_3:
+ subset s'' s=true -> subset s'' s'=true -> 
+  subset s'' (inter s s')=true.
+Proof.
+intros; apply subset_1; apply inter_subset_3; auto with set.
+Qed.
+
+(** Properties of [diff] *)
+
+Lemma diff_subset: subset (diff s s') s=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma diff_subset_equal:
+ subset s s'=true -> equal (diff s s') empty=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma remove_inter_singleton: 
+ equal (remove x s) (diff s (singleton x))=true.
+Proof.
+auto with set.
+Qed.
+
+Lemma diff_inter_empty:
+ equal (inter (diff s s') (inter s s')) empty=true. 
+Proof.
+auto with set.
+Qed.
+
+Lemma diff_inter_all: 
+ equal (union (diff s s') (inter s s')) s=true.
+Proof.
+auto with set.
+Qed.
+
+End BasicProperties.
+
+Hint Immediate empty_mem is_empty_equal_empty add_mem_1
+   remove_mem_1 singleton_equal_add union_mem inter_mem
+   diff_mem equal_sym add_remove remove_add : set. 
+Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
+   choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
+   subset_refl subset_equal subset_antisym
+   add_mem_3 add_equal remove_mem_3 remove_equal : set.
+
+
+(** General recursion principle *)
+
+Lemma set_rec:  forall (P:t->Type),
+ (forall s s', equal s s'=true -> P s -> P s') -> 
+ (forall s x, mem x s=false -> P s -> P (add x s)) -> 
+ P empty -> forall s, P s.
+Proof.
+intros.
+apply set_induction; auto; intros.
+apply X with empty; auto with set.
+apply X with (add x s0); auto with set.
+apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto.
+apply X0; auto with set; apply mem_3; auto.
+Qed.
+
+(** Properties of [fold] *)
+
+Lemma exclusive_set : forall s s' x,
+ ~(In x s/\In x s') <-> mem x s && mem x s'=false.
+Proof.
+intros; do 2 rewrite mem_iff.
+destruct (mem x s); destruct (mem x s'); intuition.
+Qed.
+
+Section Fold. 
+Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA).
+Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
+Variables (i:A).
+Variables (s s':t)(x:elt).
+ 
+Lemma fold_empty: (fold f empty i) = i.
+Proof. 
+apply fold_empty; auto.
+Qed.
+
+Lemma fold_equal: 
+ equal s s'=true -> eqA (fold f s i) (fold f s' i).
+Proof. 
+intros; apply fold_equal with (eqA:=eqA); auto with set.
+Qed.
+   
+Lemma fold_add: 
+ mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
+Proof. 
+intros; apply fold_add with (eqA:=eqA); auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma add_fold: 
+  mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
+Proof.
+intros; apply add_fold with (eqA:=eqA); auto with set.
+Qed.
+
+Lemma remove_fold_1: 
+ mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
+Proof.
+intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
+Qed.
+
+Lemma remove_fold_2: 
+ mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
+Proof.
+intros; apply remove_fold_2 with (eqA:=eqA); auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma fold_union: 
+ (forall x, mem x s && mem x s'=false) -> 
+ eqA (fold f (union s s') i) (fold f s (fold f s' i)).
+Proof.
+intros; apply fold_union with (eqA:=eqA); auto.
+intros; rewrite exclusive_set; auto.
+Qed.
+
+End Fold.
+
+(** Properties of [cardinal] *)
+
+Lemma add_cardinal_1: 
+ forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
+Proof.
+auto with set.
+Qed.
+
+Lemma add_cardinal_2: 
+ forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
+Proof.
+intros; apply add_cardinal_2; auto.
+rewrite not_mem_iff; auto.
+Qed.
+
+Lemma remove_cardinal_1: 
+ forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
+Proof.
+intros; apply remove_cardinal_1; auto with set.
+Qed.
+
+Lemma remove_cardinal_2: 
+ forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
+Proof.
+intros; apply Equal_cardinal; apply equal_2; auto with set.
+Qed.
+
+Lemma union_cardinal: 
+ forall s s', (forall x, mem x s && mem x s'=false) -> 
+ cardinal (union s s')=cardinal s+cardinal s'.
+Proof.
+intros; apply union_cardinal; auto; intros.
+rewrite exclusive_set; auto.
+Qed.
+
+Lemma subset_cardinal: 
+ forall s s', subset s s'=true -> cardinal s<=cardinal s'.
+Proof.
+intros; apply subset_cardinal; auto with set.
+Qed.
+
+Section Bool.
+
+(** Properties of [filter] *)
+
+Variable f:elt->bool.
+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.
+Qed.
+
+Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
+Proof. 
+intros; apply filter_b; auto.
+Qed.
+
+Lemma for_all_filter: 
+ forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
+Proof. 
+intros; apply bool_1; split; intros.
+apply is_empty_1.
+unfold Empty; intros. 
+rewrite filter_iff; auto.
+red; destruct 1.
+rewrite <- (@for_all_iff s f) in H; auto.
+rewrite (H a H0) in H1; discriminate.
+apply for_all_1; auto; red; intros.
+revert H; rewrite <- is_empty_iff.
+unfold Empty; intro H; generalize (H x); clear H.
+rewrite filter_iff; auto.
+destruct (f x); auto.
+Qed.
+
+Lemma exists_filter : 
+ forall s, exists_ f s=negb (is_empty (filter f s)).
+Proof. 
+intros; apply bool_1; split; intros. 
+destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).
+apply bool_6.
+red; intros; apply (@is_empty_2 _ H0 a); auto with set.
+generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)).
+destruct (choose (filter f s)).
+intros H0 _; apply exists_1; auto.
+exists e; generalize (H0 e); rewrite filter_iff; auto.
+intros _ H0.
+rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate.
+Qed.
+
+Lemma partition_filter_1: 
+ forall s, equal (fst (partition f s)) (filter f s)=true.
+Proof. 
+auto with set.
+Qed.
+
+Lemma partition_filter_2: 
+ forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
+Proof. 
+auto with set.
+Qed.
+
+Lemma filter_add_1 : forall s x, f x = true -> 
+ filter f (add x s) [=] add x (filter f s). 
+Proof.
+red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
+intuition.
+rewrite <- H; apply Comp; auto.
+Qed.
+
+Lemma filter_add_2 : forall s x, f x = false -> 
+ filter f (add x s) [=] filter f s. 
+Proof.
+red; intros; do 2 (rewrite filter_iff; auto); set_iff.
+intuition.
+assert (f x = f a) by (apply Comp; auto).
+rewrite H in H1; rewrite H2 in H1; discriminate.
+Qed.
+
+Lemma add_filter_1 : forall s s' x, 
+ f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
+Proof.
+unfold Add, MP.Add; intros.
+repeat rewrite filter_iff; auto.
+rewrite H0; clear H0.
+assert (E.eq x y -> f y = true) by 
+ (intro H0; rewrite <- (Comp _ _ H0); auto).
+tauto.
+Qed.
+
+Lemma add_filter_2 : forall s s' x, 
+ f x=false -> (Add x s s') -> filter f s [=] filter f s'.
+Proof.
+unfold Add, MP.Add, Equal; intros.
+repeat rewrite filter_iff; auto.
+rewrite H0; clear H0.
+assert (f a = true -> ~E.eq x a).
+ intros H0 H1.
+ rewrite (Comp _ _ H1) in H.
+ rewrite H in H0; discriminate.
+tauto. 
+Qed.
+
+Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
+  forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.
+Proof.
+clear Comp' Comp f.
+intros.
+assert (compat_bool E.eq (fun x => orb (f x) (g x))).
+  unfold compat_bool; 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).
+  split; auto with bool.
+  intro H3; destruct (orb_prop _ _ H3); auto.
+tauto.
+Qed.
+
+Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').
+Proof.
+unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.
+Qed.
+
+(** Properties of [for_all] *)
+
+Lemma for_all_mem_1: forall s, 
+ (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
+Proof.
+intros.
+rewrite for_all_filter; auto.
+rewrite is_empty_equal_empty.
+apply equal_mem_1;intros.
+rewrite filter_b; auto.
+rewrite empty_mem.
+generalize (H a); case (mem a s);intros;auto.
+rewrite H0;auto.
+Qed.
+
+Lemma for_all_mem_2: forall s, 
+ (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true. 
+Proof.
+intros.
+rewrite for_all_filter in H; auto.
+rewrite is_empty_equal_empty in H.
+generalize (equal_mem_2 _ _ H x).
+rewrite filter_b; auto.
+rewrite empty_mem.
+rewrite H0; simpl;intros.
+replace true with (negb false);auto;apply negb_sym;auto.
+Qed.
+
+Lemma for_all_mem_3: 
+ forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
+Proof.
+intros.
+apply (bool_eq_ind (for_all f s));intros;auto.
+rewrite for_all_filter in H1; auto.
+rewrite is_empty_equal_empty in H1.
+generalize (equal_mem_2 _ _ H1 x).
+rewrite filter_b; auto.
+rewrite empty_mem.
+rewrite H.
+rewrite H0.
+simpl;auto.
+Qed.
+
+Lemma for_all_mem_4: 
+ forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
+Proof.
+intros.
+rewrite for_all_filter in H; auto.
+destruct (choose_mem_3 _ H) as (x,(H0,H1));intros.
+exists x.
+rewrite filter_b in H1; auto.
+elim (andb_prop _ _ H1).
+split;auto.
+replace false with (negb true);auto;apply negb_sym;auto.
+Qed.
+
+(** Properties of [exists] *)
+
+Lemma for_all_exists: 
+ forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
+Proof.
+intros.
+rewrite for_all_b; auto.
+rewrite exists_b; auto.
+induction (elements s); simpl; auto.
+destruct (f a); simpl; auto.
+Qed.
+
+End Bool.
+Section Bool'.
+
+Variable f:elt->bool.
+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.
+Qed.
+
+Lemma exists_mem_1: 
+ forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
+Proof.
+intros.
+rewrite for_all_exists; auto.
+rewrite for_all_mem_1;auto with bool.
+intros;generalize (H x H0);intros. 
+symmetry;apply negb_sym;simpl;auto.
+Qed.
+
+Lemma exists_mem_2: 
+ forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false. 
+Proof.
+intros.
+rewrite for_all_exists in H; auto.
+replace false with (negb true);auto;apply negb_sym;symmetry.
+rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
+replace true with (negb false);auto;apply negb_sym;auto.
+Qed.
+
+Lemma exists_mem_3: 
+ forall s x, mem x s=true -> f x=true -> exists_ f s=true.
+Proof.
+intros.
+rewrite for_all_exists; auto.
+symmetry;apply negb_sym;simpl.
+apply for_all_mem_3 with x;auto.
+rewrite H0;auto.
+Qed.
+
+Lemma exists_mem_4: 
+ forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
+Proof.
+intros.
+rewrite for_all_exists in H; auto.
+elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros.
+elim p;intros.
+exists x;split;auto.
+replace true with (negb false);auto;apply negb_sym;auto.
+replace false with (negb true);auto;apply negb_sym;auto.
+Qed.
+
+End Bool'.
+
+Section Sum.
+
+(** Adding a valuation function on all elements of a set. *)
+
+Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. 
+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 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 (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
+assert (gc : compat_opL (fun x:elt => plus (g x))). 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 (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
+assert (st := gen_st nat).
+intros s;pattern s; apply set_rec.
+intros.
+rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
+rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H).
+rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto.
+intros; do 3 (rewrite (fold_add _ _ st);auto).
+rewrite H0;simpl;omega.
+do 3 rewrite fold_empty;auto.
+Qed.
+
+Lemma sum_filter : forall f, (compat_bool E.eq f) -> 
+  forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
+Proof.
+unfold sum; intros f Hf.
+assert (st := gen_st nat).
+assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))). 
+ red; intros.
+ rewrite (Hf x x' 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.
+intros.
+change elt with E.t.
+rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H).
+rewrite <- (MP.Equal_cardinal (filter_equal Hf (equal_2 H))); auto.
+intros; rewrite (fold_add _ _ st _ cc ct); auto.
+generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) .
+assert (~ In x (filter f s0)).
+ intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H.
+case (f x); simpl; intros.
+rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto.
+rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto.
+intros; rewrite fold_empty;auto.
+rewrite MP.cardinal_1; auto.
+unfold Empty; intros.
+rewrite filter_iff; auto; set_iff; tauto.
+Qed.
+
+Lemma fold_compat : 
+  forall (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA))
+  (f g:elt->A->A),
+  (compat_op E.eq eqA f) -> (transpose eqA f) -> 
+  (compat_op E.eq eqA g) -> (transpose eqA g) -> 
+  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> 
+  (eqA (fold f s i) (fold g s i)).
+Proof.
+intros A eqA st f g fc ft gc gt i.
+intro s; pattern s; apply set_rec; intros.
+trans_st (fold f s0 i).
+apply fold_equal with (eqA:=eqA); auto.
+rewrite equal_sym; auto.
+trans_st (fold g s0 i).
+apply H0; intros; apply H1; auto with set.
+elim  (equal_2 H x); auto with set; intros.
+apply fold_equal with (eqA:=eqA); auto with set.
+trans_st (f x (fold f s0 i)).
+apply fold_add with (eqA:=eqA); auto with set.
+trans_st (g x (fold f s0 i)); auto with set.
+trans_st (g x (fold g s0 i)); auto with set.
+sym_st; apply fold_add with (eqA:=eqA); auto.
+do 2 rewrite fold_empty; refl_st.
+Qed.
+
+Lemma sum_compat : 
+  forall f g, compat_nat E.eq f -> compat_nat E.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.
+Qed.
+
+End Sum.
+
+End EqProperties. 
diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v
index bf7f3639c4..3a8bdb032f 100644
--- a/theories/FSets/FSetWeakProperties.v
+++ b/theories/FSets/FSetWeakProperties.v
@@ -10,9 +10,6 @@
 
 (** * Finite sets library *)
 
-(** NB: this file is a clone of [FSetProperties] for weak sets
-     and should remain so until we find a way to share the two. *)
-
 (** This functor derives additional properties from [FSetWeakInterface.S].
     Contrary to the functor in [FSetWeakEqProperties] it uses 
     predicates over sets instead of sets operations, i.e.
@@ -20,7 +17,7 @@
     [Equal s s'] instead of [equal s s'=true], etc. *)
 
 Require Export FSetWeakInterface. 
-Require Import FSetWeakFacts.
+Require Import FSetWeakFacts FSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -31,418 +28,247 @@ Module Properties
  (M:FSetWeakInterface.S)
  (D:DecidableType with Definition t:=M.E.t 
                   with Definition eq:=M.E.eq).
+  Module Import FM := Facts M D.
+  Module Import Dec := FSetDecide.WeakDecide M D.
   Import M.E.
   Import M.
-  Module FM := Facts M D.
-  Import FM.
-  Import Logic. (* to unmask [eq] *)  
-  Import Peano. (* to unmask [lt] *)
-
-  (** Results about lists without duplicates *)
-
-  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
 
   Lemma In_dec : forall x s, {In x s} + {~ In x s}.
   Proof.
   intros; generalize (mem_iff s x); case (mem x s); intuition.
   Qed.
 
-  Section BasicProperties.
-
-  (** properties of [Equal] *)
-
-  Lemma equal_refl : forall s, s[=]s.
-  Proof.
-  exact eq_refl.
-  Qed.
-
-  Lemma equal_sym : forall s s', s[=]s' -> s'[=]s.
-  Proof.
-  exact eq_sym.
-  Qed.
+  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
 
-  Lemma equal_trans : forall s1 s2 s3, s1[=]s2 -> s2[=]s3 -> s1[=]s3.
+  Lemma Add_Equal : forall x s s', Add x s s' <-> s' [=] add x s.
   Proof.
-  exact eq_trans.
+  unfold Add.
+  split; intros.
+  red; intros.
+  rewrite H; clear H.
+  fsetdec.
+  fsetdec.
   Qed.
+  
+  Ltac expAdd := repeat rewrite Add_Equal.
 
-  Hint Immediate equal_refl equal_sym : set.
+  Section BasicProperties.
 
   Variable s s' s'' s1 s2 s3 : t.
   Variable x x' : elt.
 
-  (** properties of [Subset] *)
-  
+  Lemma equal_refl : s[=]s.
+  Proof. fsetdec. Qed.
+
+  Lemma equal_sym : s[=]s' -> s'[=]s.
+  Proof. fsetdec. Qed.
+
+  Lemma equal_trans : s1[=]s2 -> s2[=]s3 -> s1[=]s3.
+  Proof. fsetdec. Qed.
+
   Lemma subset_refl : s[<=]s. 
-  Proof.
-  apply Subset_refl.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
-  Proof.
-  apply Subset_trans.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
-  Proof.
-  unfold Subset, Equal; intuition.
-  Qed.
-
-  Hint Immediate subset_refl : set.
+  Proof. fsetdec. Qed.
 
   Lemma subset_equal : s[=]s' -> s[<=]s'.
-  Proof.
-  unfold Subset, Equal; intros; rewrite <- H; auto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma subset_empty : empty[<=]s.
-  Proof.
-  unfold Subset; intros a; set_iff; intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma subset_remove_3 : s1[<=]s2 -> remove x s1 [<=] s2.
-  Proof.
-  unfold Subset; intros H a; set_iff; intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma subset_diff : s1[<=]s3 -> diff s1 s2 [<=] s3.
-  Proof.
-  unfold Subset; intros H a; set_iff; intuition.
-  Qed.
-
+  Proof. fsetdec. Qed.
+ 
   Lemma subset_add_3 : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2.
-  Proof.
-  unfold Subset; intros H H0 a; set_iff; intuition.
-  rewrite <- H2; auto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma subset_add_2 : s1[<=]s2 -> s1[<=] add x s2.
-  Proof.
-  unfold Subset; intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.
-  Proof.
-  intros; rewrite <- H0; auto.
-  Qed.
+  Proof. fsetdec. Qed.
  
   Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
-  Proof.
-  unfold Subset, Equal; split; intros; intuition; generalize (H a); intuition.
-  Qed.
-
-  (** properties of [empty] *)
+  Proof. intuition fsetdec. Qed.
 
   Lemma empty_is_empty_1 : Empty s -> s[=]empty.
-  Proof.
-  unfold Empty, Equal; intros; generalize (H a); set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma empty_is_empty_2 : s[=]empty -> Empty s.
-  Proof.
-  unfold Empty, Equal; intros; generalize (H a); set_iff; tauto.
-  Qed.
-
-  (** properties of [add] *)
+  Proof. fsetdec. Qed.
 
   Lemma add_equal : In x s -> add x s [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  rewrite <- H1; auto.
-  Qed.
+  Proof. fsetdec. Qed.
  
   Lemma add_add : add x (add x' s) [=] add x' (add x s).
-  Proof. 
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
-
-  (** properties of [remove] *)
+  Proof. fsetdec. Qed.
 
   Lemma remove_equal : ~ In x s -> remove x s [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  rewrite H1 in H; auto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma Equal_remove : s[=]s' -> remove x s [=] remove x s'.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
-
-  (** properties of [add] and [remove] *)
+  Proof. fsetdec. Qed.
 
   Lemma add_remove : In x s -> add x (remove x s) [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; elim (eq_dec x a); intuition.
-  rewrite <- H1; auto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma remove_add : ~In x s -> remove x (add x s) [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; elim (eq_dec x a); intuition.
-  rewrite H1 in H; auto.
-  Qed.
-
-  (** properties of [singleton] *)
+  Proof. fsetdec. Qed.
 
   Lemma singleton_equal_add : singleton x [=] add x empty.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  Qed.
-
-  (** properties of [union] *)
+  Proof. fsetdec. Qed.
 
   Lemma union_sym : union s s' [=] union s' s.
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_subset_equal : s[<=]s' -> union s s' [=] s'.
-  Proof.
-  unfold Subset, Equal; intros; set_iff; intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_equal_1 : s[=]s' -> union s s'' [=] union s' s''.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_equal_2 : s'[=]s'' -> union s s' [=] union s s''.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_assoc : union (union s s') s'' [=] union s (union s' s'').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma add_union_singleton : add x s [=] union (singleton x) s.
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_add : union (add x s) s' [=] add x (union s s').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_remove_add_1 : 
    union (remove x s) (add x s') [=] union (add x s) (remove x s').
-  Proof.
-  unfold Equal; intros; set_iff.
-  destruct (eq_dec x a); intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_remove_add_2 : In x s -> 
    union (remove x s) (add x s') [=] union s s'.
-  Proof.
-  unfold Equal; intros; set_iff.
-  destruct (eq_dec x a); intuition.
-  left; eauto with set.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_subset_1 : s [<=] union s s'.
-  Proof.
-  unfold Subset; intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_subset_2 : s' [<=] union s s'.
-  Proof.
-  unfold Subset; intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_subset_3 : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s''.
-  Proof.
-  unfold Subset; intros H H0 a; set_iff; intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_subset_4 : s[<=]s' -> union s s'' [<=] union s' s''.
-  Proof. 
-  unfold Subset; intros H a; set_iff; intuition.
-  Qed.
+  Proof. fsetdec. Qed. 
 
   Lemma union_subset_5 : s[<=]s' -> union s'' s [<=] union s'' s'.
-  Proof. 
-  unfold Subset; intros H a; set_iff; intuition.
-  Qed.
+  Proof. fsetdec. Qed. 
 
   Lemma empty_union_1 : Empty s -> union s s' [=] s'.
-  Proof.
-  unfold Equal, Empty; intros; set_iff; firstorder.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma empty_union_2 : Empty s -> union s' s [=] s'.
-  Proof.
-  unfold Equal, Empty; intros; set_iff; firstorder.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma not_in_union : ~In x s -> ~In x s' -> ~In x (union s s'). 
-  Proof.
-  intros; set_iff; intuition. 
-  Qed.  
-
-  (** properties of [inter] *)
+  Proof. fsetdec. Qed.
 
   Lemma inter_sym : inter s s' [=] inter s' s.
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma inter_subset_equal : s[<=]s' -> inter s s' [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma inter_equal_1 : s[=]s' -> inter s s'' [=] inter s' s''.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma inter_equal_2 : s'[=]s'' -> inter s s' [=] inter s s''.
-  Proof.
-  intros; rewrite H; apply equal_refl.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma inter_assoc : inter (inter s s') s'' [=] inter s (inter s' s'').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_inter_1 : inter (union s s') s'' [=] union (inter s s'') (inter s' s'').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma union_inter_2 : union (inter s s') s'' [=] inter (union s s'') (union s' s'').
-  Proof.
-  unfold Equal; intros; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma inter_add_1 : In x s' -> inter (add x s) s' [=] add x (inter s s').
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  rewrite <- H1; auto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma inter_add_2 : ~ In x s' -> inter (add x s) s' [=] inter s s'.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  destruct H; rewrite H0; auto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma empty_inter_1 : Empty s -> Empty (inter s s').
-  Proof.
-  unfold Empty; intros; set_iff; firstorder.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma empty_inter_2 : Empty s' -> Empty (inter s s').
-  Proof.
-  unfold Empty; intros; set_iff; firstorder.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma inter_subset_1 : inter s s' [<=] s.
-  Proof.
-  unfold Subset; intro a; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma inter_subset_2 : inter s s' [<=] s'.
-  Proof.
-  unfold Subset; intro a; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma inter_subset_3 :
    s''[<=]s -> s''[<=]s' -> s''[<=] inter s s'.
-  Proof.
-  unfold Subset; intros H H' a; set_iff; intuition.
-  Qed.
-
-  (** properties of [diff] *)
+  Proof. fsetdec. Qed.
 
   Lemma empty_diff_1 : Empty s -> Empty (diff s s'). 
-  Proof.
-  unfold Empty, Equal; intros; set_iff; firstorder.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma empty_diff_2 : Empty s -> diff s' s [=] s'.
-  Proof.
-  unfold Empty, Equal; intros; set_iff; firstorder.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma diff_subset : diff s s' [<=] s.
-  Proof.
-  unfold Subset; intros a; set_iff; tauto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma diff_subset_equal : s[<=]s' -> diff s s' [=] empty.
-  Proof.
-  unfold Subset, Equal; intros; set_iff; intuition; absurd (In a empty); auto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma remove_diff_singleton :
    remove x s [=] diff s (singleton x).
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma diff_inter_empty : inter (diff s s') (inter s s') [=] empty. 
-  Proof.
-  unfold Equal; intros; set_iff; intuition; absurd (In a empty); auto.
-  Qed.
+  Proof. fsetdec. Qed.
 
   Lemma diff_inter_all : union (diff s s') (inter s s') [=] s.
-  Proof.
-  unfold Equal; intros; set_iff; intuition.
-  elim (In_dec a s'); auto.
-  Qed.
-
-  (** properties of [Add] *)
+  Proof. fsetdec. Qed.
 
   Lemma Add_add : Add x s (add x s).
-  Proof.
-   unfold Add; intros; set_iff; intuition.
-  Qed.
+  Proof. expAdd; fsetdec. Qed.
 
   Lemma Add_remove : In x s -> Add x (remove x s) s. 
-  Proof. 
-    unfold Add; intros; set_iff; intuition.
-    elim (eq_dec x y); auto.
-    rewrite <- H1; auto.
-  Qed.
+  Proof. expAdd; fsetdec. Qed.
 
   Lemma union_Add : Add x s s' -> Add x (union s s'') (union s' s'').
-  Proof. 
-  unfold Add; intros; set_iff; rewrite H; tauto.
-  Qed.
+  Proof. expAdd; fsetdec. Qed. 
 
   Lemma inter_Add :
    In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'').
-  Proof. 
-  unfold Add; intros; set_iff; rewrite H0; intuition.
-  rewrite <- H2; auto.
-  Qed.  
+  Proof. expAdd; fsetdec. Qed. 
 
   Lemma union_Equal :
    In x s'' -> Add x s s' -> union s s'' [=] union s' s''.
-  Proof. 
-  unfold Add, Equal; intros; set_iff; rewrite H0; intuition. 
-  rewrite <- H1; auto.
-  Qed.  
+  Proof. expAdd; fsetdec. Qed. 
 
   Lemma inter_Add_2 :
    ~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s''.
-  Proof.
-  unfold Add, Equal; intros; set_iff; rewrite H0; intuition.
-  destruct H; rewrite H1; auto.
-  Qed.
+  Proof. expAdd; fsetdec. Qed.
 
   End BasicProperties.
 
-  Hint Immediate equal_sym: set.
-  Hint Resolve equal_refl equal_trans : set.
-
-  Hint Immediate add_remove remove_add union_sym inter_sym: set.
-  Hint Resolve subset_refl subset_equal subset_antisym 
+  Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
+  Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym 
     subset_trans subset_empty subset_remove_3 subset_diff subset_add_3 
     subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
     remove_equal singleton_equal_add union_subset_equal union_equal_1 
@@ -455,6 +281,26 @@ Module Properties
     remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
     Equal_remove add_add : set.
 
+  (** * Properties of elements *)
+
+  Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
+  Proof.
+  intros.
+  unfold Empty.
+  split; intros.
+  assert (forall a, ~ List.In a (elements s)).
+   red; intros.
+   apply (H a).
+   rewrite elements_iff.
+   rewrite InA_alt; exists a; auto.
+  destruct (elements s); auto.
+  elim (H0 e); simpl; auto.
+  red; intros.
+  rewrite elements_iff in H0.
+  rewrite InA_alt in H0; destruct H0.
+  rewrite H in H0; destruct H0 as (_,H0); inversion H0.
+  Qed.
+
   (** * Alternative (weaker) specifications for [fold] *)
 
   Section Old_Spec_Now_Properties. 
@@ -516,6 +362,18 @@ Module Properties
    rewrite (H2 a); intuition.
   Qed.
 
+  (** In fact, [fold] on empty sets is more than equivalent to 
+      the initial element, it is Leibniz-equal to it. *)
+
+  Lemma fold_1b :
+   forall s (A : Set)(i : A) (f : elt -> A -> A),
+   Empty s -> (fold f s i) = i.
+  Proof.
+  intros.
+  rewrite M.fold_1.
+  rewrite elements_Empty in H; rewrite H; simpl; auto.
+  Qed.
+
   (** Similar specifications for [cardinal]. *)
 
   Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
@@ -550,51 +408,46 @@ Module Properties
 
   (** * Induction principle over sets *)
 
+  Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
+  Proof.
+  intros.
+  rewrite elements_Empty, M.cardinal_1.
+  destruct (elements s); intuition; discriminate.
+  Qed.
+
   Lemma cardinal_inv_1 : forall s, cardinal s = 0 -> Empty s. 
-  Proof. 
-    intros s; rewrite M.cardinal_1; intros H a; red.
-    rewrite elements_iff.
-    destruct (elements s); simpl in *; discriminate || inversion 1.
+  Proof.
+  intros; rewrite cardinal_Empty; auto. 
   Qed.
   Hint Resolve cardinal_inv_1.
  
   Lemma cardinal_inv_2 :
    forall s n, cardinal s = S n -> { x : elt | In x s }.
   Proof. 
-    intros; rewrite M.cardinal_1 in H.
-    generalize (elements_2 (s:=s)).
-    destruct (elements s); try discriminate. 
-    exists e; auto.
+  intros; rewrite M.cardinal_1 in H.
+  generalize (elements_2 (s:=s)).
+  destruct (elements s); try discriminate. 
+  exists e; auto.
   Qed.
 
   Lemma cardinal_inv_2b :
    forall s, cardinal s <> 0 -> { x : elt | In x s }.
   Proof.
-    intros; rewrite M.cardinal_1 in H.
-    generalize (elements_2 (s:=s)).
-    destruct (elements s); simpl in H.
-    elim H; auto.
-    exists e; auto.
-  Qed.
-
-  Lemma Equal_cardinal_aux :
-   forall n s s', cardinal s = n -> s[=]s' -> cardinal s = cardinal s'.
-  Proof.
-     simple induction n; intros.
-     rewrite H; symmetry .
-     apply cardinal_1.
-     rewrite <- H0; auto.
-     destruct (cardinal_inv_2 H0) as (x,H2).
-     revert H0.
-     rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.
-     rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); auto with set.
-     rewrite H1 in H2; auto with set.
+  intro; generalize (@cardinal_inv_2 s); destruct cardinal; 
+   [intuition|eauto].
   Qed.
 
   Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
   Proof. 
-    intros; apply Equal_cardinal_aux with (cardinal s); auto.
-  Qed.
+  symmetry.
+  remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H.
+  induction n; intros.
+  apply cardinal_1; rewrite <- H; auto.
+  destruct (cardinal_inv_2 Heqn) as (x,H2).
+  revert Heqn.
+  rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.
+  rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set.
+  Qed.    
 
   Add Morphism cardinal : cardinal_m.
   Proof.
@@ -603,27 +456,20 @@ Module Properties
 
   Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
 
-  Lemma cardinal_induction :
-   forall P : t -> Type,
-   (forall s, Empty s -> P s) ->
-   (forall s s', P s -> forall x, ~In x s -> Add x s s' -> P s') ->
-   forall n s, cardinal s = n -> P s.
-  Proof.
-  simple induction n; intros; auto.
-  destruct (cardinal_inv_2 H) as (x,H0). 
-  apply X0 with (remove x s) x; auto with set.
-  apply X1; auto with set.
-  rewrite (cardinal_2 (x:=x)(s:=remove x s)(s':=s)) in H; auto with set.
-  Qed.
-
   Lemma set_induction :
    forall P : t -> Type,
    (forall s : t, Empty s -> P s) ->
    (forall s s' : t, P s -> forall x : elt, ~In x s -> Add x s s' -> P s') ->
    forall s : t, P s.
   Proof.
-  intros; apply cardinal_induction with (cardinal s); auto.
-  Qed.  
+  intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto.
+  destruct (cardinal_inv_2 (sym_eq Heqn)) as (x,H0). 
+  apply X0 with (remove x s) x; auto with set.
+  apply IHn; auto.
+  assert (S n = S (cardinal (remove x s))).
+    rewrite Heqn; apply cardinal_2 with x; auto with set.
+  inversion H; auto.
+  Qed.
 
   (** Other properties of [fold]. *)
 
@@ -634,9 +480,9 @@ Module Properties
   Section Fold_1. 
   Variable i i':A.
 
-  Lemma fold_empty : eqA (fold f empty i) i.
+  Lemma fold_empty : (fold f empty i) = i.
   Proof. 
-  apply fold_1; auto with set.
+  apply fold_1b; auto with set.
   Qed.
 
   Lemma fold_equal : 
@@ -790,8 +636,8 @@ Module Properties
    forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
   Proof.
   assert (st := gen_st nat).
-  assert (fe : compat_op E.eq (@eq _) (fun _ => S)) by (unfold compat_op; auto). 
-  assert (fp : transpose (@eq _) (fun _:elt => S)) by (unfold transpose; auto).
+  assert (fe : compat_op E.eq (@Logic.eq _) (fun _ => S)) by (unfold compat_op; auto). 
+  assert (fp : transpose (@Logic.eq _) (fun _:elt => S)) by (unfold transpose; auto).
   intros s p; pattern s; apply set_induction; clear s; intros.
   rewrite (fold_1 st p (fun _ => S) H).
   rewrite (fold_1 st 0 (fun _ => S) H); trivial.
@@ -804,7 +650,7 @@ Module Properties
   simpl; auto.
   Qed.
 
-  (** properties of [cardinal] *)
+  (** more properties of [cardinal] *)
 
   Lemma empty_cardinal : cardinal empty = 0.
   Proof.
@@ -828,7 +674,7 @@ Module Properties
   Proof.
   intros; do 3 rewrite cardinal_fold.
   rewrite <- fold_plus.
-  apply fold_diff_inter with (eqA:=@eq nat); auto.
+  apply fold_diff_inter with (eqA:=@Logic.eq nat); auto.
   Qed.
 
   Lemma union_cardinal: 
@@ -871,7 +717,7 @@ Module Properties
   intros.
   do 4 rewrite cardinal_fold.
   do 2 rewrite <- fold_plus.
-  apply fold_union_inter with (eqA:=@eq nat); auto.
+  apply fold_union_inter with (eqA:=@Logic.eq nat); auto.
   Qed.
 
   Lemma union_cardinal_inter : 
@@ -902,7 +748,7 @@ Module Properties
   intros.
   do 2 rewrite cardinal_fold.
   change S with ((fun _ => S) x);
-   apply fold_add with (eqA:=@eq nat); auto.
+   apply fold_add with (eqA:=@Logic.eq nat); auto.
   Qed.
 
   Lemma remove_cardinal_1 :
@@ -911,7 +757,7 @@ Module Properties
   intros.
   do 2 rewrite cardinal_fold.
   change S with ((fun _ =>S) x).
-  apply remove_fold_1 with (eqA:=@eq nat); auto.
+  apply remove_fold_1 with (eqA:=@Logic.eq nat); auto.
   Qed.
 
   Lemma remove_cardinal_2 : 
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 1995ca77a4..6f793ce2fa 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -12,49 +12,184 @@
 Definition decidable (P:Prop) := P \/ ~ P.
 
 Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P.
-unfold decidable in |- *; tauto. 
+Proof.
+unfold decidable; tauto. 
 Qed.
 
 Theorem dec_True : decidable True.
-unfold decidable in |- *; auto.
+Proof.
+unfold decidable; auto.
 Qed.
 
 Theorem dec_False : decidable False.
-unfold decidable, not in |- *; auto.
+Proof.
+unfold decidable, not; auto.
 Qed.
 
 Theorem dec_or :
  forall A B:Prop, decidable A -> decidable B -> decidable (A \/ B).
-unfold decidable in |- *; tauto. 
+Proof.
+unfold decidable; tauto. 
 Qed.
 
 Theorem dec_and :
  forall A B:Prop, decidable A -> decidable B -> decidable (A /\ B).
-unfold decidable in |- *; tauto. 
+Proof.
+unfold decidable; tauto. 
 Qed.
 
 Theorem dec_not : forall A:Prop, decidable A -> decidable (~ A).
-unfold decidable in |- *; tauto. 
+Proof.
+unfold decidable; tauto. 
 Qed.
 
 Theorem dec_imp :
  forall A B:Prop, decidable A -> decidable B -> decidable (A -> B).
-unfold decidable in |- *; tauto. 
+Proof.
+unfold decidable; tauto. 
+Qed.
+
+Theorem dec_iff : 
+ forall A B:Prop, decidable A -> decidable B -> decidable (A<->B).
+Proof.
+unfold decidable; tauto.
 Qed.
 
 Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P.
-unfold decidable in |- *; tauto. Qed.
+Proof.
+unfold decidable; tauto.
+Qed.
 
 Theorem not_or : forall A B:Prop, ~ (A \/ B) -> ~ A /\ ~ B.
-tauto. Qed.
+Proof.
+tauto.
+Qed.
 
 Theorem not_and : forall A B:Prop, decidable A -> ~ (A /\ B) -> ~ A \/ ~ B.
-unfold decidable in |- *; tauto. Qed.
+Proof.
+unfold decidable; tauto. 
+Qed.
 
 Theorem not_imp : forall A B:Prop, decidable A -> ~ (A -> B) -> A /\ ~ B.
-unfold decidable in |- *; tauto.
+Proof.
+unfold decidable; tauto.
 Qed.
 
 Theorem imp_simp : forall A B:Prop, decidable A -> (A -> B) -> ~ A \/ B.
-unfold decidable in |- *; tauto.
+Proof.
+unfold decidable; tauto.
+Qed.
+
+(** Results formulated with iff, used in FSetDecide. 
+    Negation are expanded since it is unclear whether setoid rewrite 
+    will always perform conversion. *)    
+
+(** We begin with lemmas that, when read from left to right,
+    can be understood as ways to eliminate uses of [not]. *)
+
+Theorem not_true_iff : (True -> False) <-> False.
+Proof.
+tauto.
+Qed.
+
+Theorem not_false_iff : (False -> False) <-> True.
+Proof.
+tauto.
+Qed.
+
+Theorem not_not_iff : forall A:Prop, decidable A ->
+  (((A -> False) -> False) <-> A).
+Proof.
+unfold decidable; tauto.
+Qed.
+
+Theorem contrapositive : forall A B:Prop, decidable A ->
+  (((A -> False) -> (B -> False)) <-> (B -> A)).
+Proof.
+unfold decidable; tauto.
+Qed.
+
+Lemma or_not_l_iff_1 : forall A B: Prop, decidable A ->
+  ((A -> False) \/ B <-> (A -> B)).
+Proof.
+unfold decidable. tauto.
+Qed.
+
+Lemma or_not_l_iff_2 : forall A B: Prop, decidable B ->
+  ((A -> False) \/ B <-> (A -> B)).
+Proof.
+unfold decidable. tauto.
+Qed.
+
+Lemma or_not_r_iff_1 : forall A B: Prop, decidable A ->
+  (A \/ (B -> False) <-> (B -> A)).
+Proof.
+unfold decidable. tauto.
 Qed.
+
+Lemma or_not_r_iff_2 : forall A B: Prop, decidable B ->
+  (A \/ (B -> False) <-> (B -> A)).
+Proof.
+unfold decidable. tauto.
+Qed.
+
+Lemma imp_not_l : forall A B: Prop, decidable A ->
+  (((A -> False) -> B) <-> (A \/ B)).
+Proof.
+unfold decidable. tauto.
+Qed.
+
+
+(** Moving Negations Around:
+    We have four lemmas that, when read from left to right,
+    describe how to push negations toward the leaves of a
+    proposition and, when read from right to left, describe
+    how to pull negations toward the top of a proposition. *)
+
+Theorem not_or_iff : forall A B:Prop,
+  (A \/ B -> False) <-> (A -> False) /\ (B -> False).
+Proof.
+tauto.
+Qed.
+
+Lemma not_and_iff : forall A B:Prop,
+  (A /\ B -> False) <-> (A -> B -> False).
+Proof.
+tauto.
+Qed.
+
+Lemma not_imp_iff : forall A B:Prop, decidable A ->
+  (((A -> B) -> False) <-> A /\ (B -> False)).
+Proof.
+unfold decidable. tauto.
+Qed.
+
+Lemma not_imp_rev_iff : forall A B : Prop, decidable A ->
+  (((A -> B) -> False) <-> (B -> False) /\ A).
+Proof.
+unfold decidable. tauto.
+Qed.
+
+
+
+(** With the following hint database, we can leverage [auto] to check
+    decidability of propositions. *)
+
+Hint Resolve dec_True dec_False dec_or dec_and dec_imp dec_not dec_iff
+ : decidable_prop.
+
+(** [solve_decidable using lib] will solve goals about the
+    decidability of a proposition, assisted by an auxiliary
+    database of lemmas.  The database is intended to contain
+    lemmas stating the decidability of base propositions,
+    (e.g., the decidability of equality on a particular
+    inductive type). *)
+
+Tactic Notation "solve_decidable" "using" ident(db) :=
+  match goal with
+   | |- decidable _ =>
+     solve [ auto 100 with decidable_prop db ]
+  end.
+
+Tactic Notation "solve_decidable" :=
+  solve_decidable using core.