Introducing MMaps, a modernized FMaps.

 NB: this is work-in-progress, there is currently only one
 provided implementation (MMapWeakList).

 In the same spirit as MSets w.r.t FSets, the main difference between
 MMaps and former FMaps is the use of a new version of OrderedType
 (see Orders.v instead of obsolete OrderedType.v).

 We also try to benefit more from recent notions such as Proper.

 For most function specifications, the style has changed : we now use
 equations over "find" instead of "MapsTo" predicates, whenever possible
 (cf. Maps in Compcert for a source of inspiration). Former specs are
 now derived in FMapFacts, so this is mostly a matter of taste.

 Two changes inspired by the current Maps of OCaml:
 - "elements" is now "bindings"
 - "map2" is now "merge" (and its function argument also receives a key).

 We now use a maximal implicit argument for "empty".

2 files changed, 181 insertions, 244 deletions

diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index 11d94c119..b394cf48d 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -8,132 +8,170 @@
 
 Require Import Equalities Bool SetoidList RelationPairs.
 
-(** * Keys and datas used in FMap *)
+(** * Keys and datas used in MMap *)
 
-Module KeyDecidableType(Import D:DecidableType).
+Module KeyDecidableType(D:DecidableType).
 
- Section Elt.
- Variable elt : Type.
- Notation key:=t.
+ Local Open Scope signature_scope.
+ Local Notation key := D.t.
 
-  Local Open Scope signature_scope.
+ Definition eqk {elt} : relation (key*elt) := D.eq @@1.
+ Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq.
 
-  Definition eqk : relation (key*elt) := eq @@1.
-  Definition eqke : relation (key*elt) := eq * Logic.eq.
-  Hint Unfold eqk eqke.
+ Hint Unfold eqk eqke.
 
-  (* eqke is stricter than eqk *)
+ (** eqk, eqke are equalities *)
 
-  Global Instance eqke_eqk : subrelation eqke eqk.
-  Proof. firstorder. Qed.
+ Instance eqk_equiv {elt} : Equivalence (@eqk elt) := _.
 
-  (* eqk, eqke are equalities, ltk is a strict order *)
+ Instance eqke_equiv {elt} : Equivalence (@eqke elt) := _.
 
-  Global Instance eqk_equiv : Equivalence eqk := _.
+ (** eqke is stricter than eqk *)
 
-  Global Instance eqke_equiv : Equivalence eqke := _.
+ Instance eqke_eqk {elt} : subrelation (@eqke elt) (@eqk elt).
+ Proof. firstorder. Qed.
 
-  (* Additionnal facts *)
+ (** Alternative definitions of eqke and eqk *)
 
-  Lemma InA_eqke_eqk :
-     forall x m, InA eqke x m -> InA eqk x m.
-  Proof.
-    unfold eqke, RelProd; induction 1; firstorder.
-  Qed.
-  Hint Resolve InA_eqke_eqk.
+ Lemma eqke_def {elt} k k' (e e':elt) :
+  eqke (k,e) (k',e') = (D.eq k k' /\ e = e').
+ Proof. reflexivity. Defined.
 
-  Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
-  Proof.
-   intros. rewrite <- H; auto.
-  Qed.
+ Lemma eqke_def' {elt} (p q:key*elt) :
+  eqke p q = (D.eq (fst p) (fst q) /\ snd p = snd q).
+ Proof. reflexivity. Defined.
 
-  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
-  Definition In k m := exists e:elt, MapsTo k e m.
+ Lemma eqke_1 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> D.eq k k'.
+ Proof. now destruct 1. Qed.
 
-  Hint Unfold MapsTo In.
+ Lemma eqke_2 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> e=e'.
+ Proof. now destruct 1. Qed.
 
-  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
+ Lemma eqk_def {elt} k k' (e e':elt) : eqk (k,e) (k',e') = D.eq k k'.
+ Proof. reflexivity. Defined.
 
-  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
-  Proof.
-  firstorder.
-  exists x; auto.
-  induction H.
-  destruct y; compute in H.
-  exists e; left; auto.
-  destruct IHInA as [e H0].
-  exists e; auto.
-  Qed.
-
-  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
-  Proof.
+ Lemma eqk_def' {elt} (p q:key*elt) : eqk p q = D.eq (fst p) (fst q).
+ Proof. reflexivity. Qed.
+
+ Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'.
+ Proof. trivial. Qed.
+
+ Hint Resolve eqke_1 eqke_2 eqk_1.
+
+ (* Additionnal facts *)
+
+ Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) :
+   InA eqke p m -> InA eqk p m.
+ Proof.
+  induction 1; firstorder.
+ Qed.
+ Hint Resolve InA_eqke_eqk.
+
+ Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) :
+  InA eqk p m -> exists q, eqk p q /\ InA eqke q m.
+ Proof.
+  induction 1; firstorder.
+ Qed.
+
+ Lemma InA_eqk {elt} p q (m:list (key*elt)) :
+   eqk p q -> InA eqk p m -> InA eqk q m.
+ Proof.
+  now intros <-.
+ Qed.
+
+ Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e).
+ Definition In {elt} k m := exists e:elt, MapsTo k e m.
+
+ Hint Unfold MapsTo In.
+
+ (* Alternative formulations for [In k l] *)
+
+ Lemma In_alt {elt} k (l:list (key*elt)) :
+   In k l <-> exists e, InA eqk (k,e) l.
+ Proof.
+  unfold In, MapsTo.
+  split; intros (e,H).
+  - exists e; auto.
+  - apply InA_eqk_eqke in H. destruct H as ((k',e'),(E,H)).
+    compute in E. exists e'. now rewrite E.
+ Qed.
+
+ Lemma In_alt' {elt} (l:list (key*elt)) k e :
+   In k l <-> InA eqk (k,e) l.
+ Proof.
+  rewrite In_alt. firstorder. eapply InA_eqk; eauto. now compute.
+ Qed.
+
+ Lemma In_alt2 {elt} k (l:list (key*elt)) :
+   In k l <-> Exists (fun p => D.eq k (fst p)) l.
+ Proof.
   unfold In, MapsTo.
   setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
   firstorder.
   exists (snd x), x; auto.
-  Qed.
-
-  Lemma In_nil : forall k, In k nil <-> False.
-  Proof.
-  intros; rewrite In_alt2; apply Exists_nil.
-  Qed.
-
-  Lemma In_cons : forall k p l,
-   In k (p::l) <-> eq k (fst p) \/ In k l.
-  Proof.
-  intros; rewrite !In_alt2, Exists_cons; intuition.
-  Qed.
-
-  Global Instance MapsTo_compat :
-   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
-  Proof.
+ Qed.
+
+ Lemma In_nil {elt} k : In k (@nil (key*elt)) <-> False.
+ Proof.
+  rewrite In_alt2; apply Exists_nil.
+ Qed.
+
+ Lemma In_cons {elt} k p (l:list (key*elt)) :
+   In k (p::l) <-> D.eq k (fst p) \/ In k l.
+ Proof.
+  rewrite !In_alt2, Exists_cons; intuition.
+ Qed.
+
+ Instance MapsTo_compat {elt} :
+   Proper (D.eq==>Logic.eq==>equivlistA eqke==>iff) (@MapsTo elt).
+ Proof.
   intros x x' Hx e e' He l l' Hl. unfold MapsTo.
   rewrite Hx, He, Hl; intuition.
-  Qed.
+ Qed.
 
-  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
-  Proof.
+ Instance In_compat {elt} : Proper (D.eq==>equivlistA eqk==>iff) (@In elt).
+ Proof.
   intros x x' Hx l l' Hl. rewrite !In_alt.
   setoid_rewrite Hl. setoid_rewrite Hx. intuition.
-  Qed.
-
-  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
-  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
+ Qed.
 
-  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
+ Lemma MapsTo_eq {elt} (l:list (key*elt)) x y e :
+   D.eq x y -> MapsTo x e l -> MapsTo y e l.
+ Proof. now intros <-. Qed.
 
-  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
-  Proof.
-    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
-    right; exists x; auto.
-  Qed.
+ Lemma In_eq {elt} (l:list (key*elt)) x y :
+   D.eq x y -> In x l -> In y l.
+ Proof. now intros <-. Qed.
 
-  Lemma In_inv_2 : forall k k' e e' l,
-      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
-  Proof.
-   intros; invlist InA; intuition.
-  Qed.
+ Lemma In_inv {elt} k k' e (l:list (key*elt)) :
+   In k ((k',e) :: l) -> D.eq k k' \/ In k l.
+ Proof.
+  intros (e',H). red in H. rewrite InA_cons, eqke_def in H.
+  intuition. right. now exists e'.
+ Qed.
 
-  Lemma In_inv_3 : forall x x' l,
-      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
-  Proof.
-   intros; invlist InA; compute in * |- ; intuition.
-  Qed.
+ Lemma In_inv_2 {elt} k k' e e' (l:list (key*elt)) :
+   InA eqk (k, e) ((k', e') :: l) -> ~ D.eq k k' -> InA eqk (k, e) l.
+ Proof.
+  rewrite InA_cons, eqk_def. intuition.
+ Qed.
 
- End Elt.
+ Lemma In_inv_3 {elt} x x' (l:list (key*elt)) :
+   InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
+ Proof.
+  rewrite InA_cons. destruct 1 as [H|H]; trivial. destruct 1.
+  eauto with *.
+ Qed.
 
- Hint Unfold eqk eqke.
  Hint Extern 2 (eqke ?a ?b) => split.
  Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
  Hint Resolve In_inv_2 In_inv_3.
 
 End KeyDecidableType.
 
 
-(** * PairDecidableType 
-   
+(** * PairDecidableType
+
    From two decidable types, we can build a new DecidableType
    over their cartesian product. *)
 
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index 059992f5b..4d49ac84e 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -6,51 +6,47 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Export RelationPairs SetoidList Orders.
+Require Export RelationPairs SetoidList Orders EqualitiesFacts.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 (** * Specialization of results about lists modulo. *)
 
-Module OrderedTypeLists (Import O:OrderedType).
+Module OrderedTypeLists (O:OrderedType).
 
-Section ForNotations.
-
-Notation In:=(InA eq).
-Notation Inf:=(lelistA lt).
-Notation Sort:=(sort lt).
-Notation NoDup:=(NoDupA eq).
+Local Notation In:=(InA O.eq).
+Local Notation Inf:=(lelistA O.lt).
+Local Notation Sort:=(sort O.lt).
+Local Notation NoDup:=(NoDupA O.eq).
 
 Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
 Proof. intros. rewrite <- H; auto. Qed.
 
 Lemma ListIn_In : forall l x, List.In x l -> In x l.
-Proof. exact (In_InA eq_equiv). Qed.
+Proof. exact (In_InA O.eq_equiv). Qed.
 
-Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_ltA lt_strorder). Qed.
+Lemma Inf_lt : forall l x y, O.lt x y -> Inf y l -> Inf x l.
+Proof. exact (InfA_ltA O.lt_strorder). Qed.
 
-Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_compat). Qed.
+Lemma Inf_eq : forall l x y, O.eq x y -> Inf y l -> Inf x l.
+Proof. exact (InfA_eqA O.eq_equiv O.lt_compat). Qed.
 
-Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
-Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
+Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> O.lt a x.
+Proof. exact (SortA_InfA_InA O.eq_equiv O.lt_strorder O.lt_compat). Qed.
 
-Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.
-Proof. exact (@In_InfA t lt). Qed.
+Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> O.lt x y) -> Inf x l.
+Proof. exact (@In_InfA O.t O.lt). Qed.
 
-Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.
-Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed.
+Lemma In_Inf : forall l x, (forall y, In y l -> O.lt x y) -> Inf x l.
+Proof. exact (InA_InfA O.eq_equiv (ltA:=O.lt)). Qed.
 
 Lemma Inf_alt :
- forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
-Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed.
+ forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> O.lt x y)).
+Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed.
 
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
-Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed.
-
-End ForNotations.
+Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed.
 
 Hint Resolve ListIn_In Sort_NoDup Inf_lt.
 Hint Immediate In_eq Inf_lt.
@@ -58,140 +54,66 @@ Hint Immediate In_eq Inf_lt.
 End OrderedTypeLists.
 
 
+(** * Results about keys and data as manipulated in MMaps. *)
 
+Module KeyOrderedType(O:OrderedType).
+ Include KeyDecidableType(O). (* provides eqk, eqke *)
 
+ Local Notation key:=O.t.
+ Local Open Scope signature_scope.
 
-(** * Results about keys and data as manipulated in FMaps. *)
-
-
-Module KeyOrderedType(Import O:OrderedType).
- Module Import MO:=OrderedTypeLists(O).
-
- Section Elt.
- Variable elt : Type.
- Notation key:=t.
-
-  Local Open Scope signature_scope.
-
-  Definition eqk : relation (key*elt) := eq @@1.
-  Definition eqke : relation (key*elt) := eq * Logic.eq.
-  Definition ltk : relation (key*elt) := lt @@1.
-
-  Hint Unfold eqk eqke ltk.
+ Definition ltk {elt} : relation (key*elt) := O.lt @@1.
 
-  (* eqke is stricter than eqk *)
+ Hint Unfold ltk.
 
-  Global Instance eqke_eqk : subrelation eqke eqk.
-  Proof. firstorder. Qed.
+ (* ltk is a strict order *)
 
-  (* eqk, eqke are equalities, ltk is a strict order *)
+ Instance ltk_strorder {elt} : StrictOrder (@ltk elt) := _.
 
-  Global Instance eqk_equiv : Equivalence eqk := _.
+ Instance ltk_compat {elt} : Proper (eqk==>eqk==>iff) (@ltk elt).
+ Proof. unfold eqk, ltk; auto with *. Qed.
 
-  Global Instance eqke_equiv : Equivalence eqke := _.
+ Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt).
+ Proof. eapply subrelation_proper; eauto with *. Qed.
 
-  Global Instance ltk_strorder : StrictOrder ltk := _.
+ (* Additionnal facts *)
 
-  Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
-  Proof. unfold eqk, ltk; auto with *. Qed.
+ Instance pair_compat {elt} : Proper (O.eq==>Logic.eq==>eqke) (@pair key elt).
+ Proof. apply pair_compat. Qed.
 
-  (* Additionnal facts *)
-
-  Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt).
-  Proof. apply pair_compat. Qed.
+ Section Elt.
+  Variable elt : Type.
+  Implicit Type p q : key*elt.
+  Implicit Type l m : list (key*elt).
 
-  Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
+  Lemma ltk_not_eqk p q : ltk p q -> ~ eqk p q.
   Proof.
-  intros e e' LT EQ; rewrite EQ in LT.
+  intros LT EQ; rewrite EQ in LT.
   elim (StrictOrder_Irreflexive _ LT).
   Qed.
 
-  Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
+  Lemma ltk_not_eqke p q : ltk p q -> ~eqke p q.
   Proof.
-  intros e e' LT EQ; rewrite EQ in LT.
+  intros LT EQ; rewrite EQ in LT.
   elim (StrictOrder_Irreflexive _ LT).
   Qed.
 
-  Lemma InA_eqke_eqk :
-     forall x m, InA eqke x m -> InA eqk x m.
-  Proof.
-    unfold eqke, RelProd; induction 1; firstorder.
-  Qed.
-  Hint Resolve InA_eqke_eqk.
-
-  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
-  Definition In k m := exists e:elt, MapsTo k e m.
   Notation Sort := (sort ltk).
   Notation Inf := (lelistA ltk).
 
-  Hint Unfold MapsTo In.
-
-  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
-
-  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
-  Proof.
-  firstorder.
-  exists x; auto.
-  induction H.
-  destruct y; compute in H.
-  exists e; left; auto.
-  destruct IHInA as [e H0].
-  exists e; auto.
-  Qed.
+  Lemma Inf_eq l x x' : eqk x x' -> Inf x' l -> Inf x l.
+  Proof. now intros <-. Qed.
 
-  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
-  Proof.
-  unfold In, MapsTo.
-  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
-  firstorder.
-  exists (snd x), x; auto.
-  Qed.
-
-  Lemma In_nil : forall k, In k nil <-> False.
-  Proof.
-  intros; rewrite In_alt2; apply Exists_nil.
-  Qed.
-
-  Lemma In_cons : forall k p l,
-   In k (p::l) <-> eq k (fst p) \/ In k l.
-  Proof.
-  intros; rewrite !In_alt2, Exists_cons; intuition.
-  Qed.
-
-  Global Instance MapsTo_compat :
-   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
-  Proof.
-  intros x x' Hx e e' He l l' Hl. unfold MapsTo.
-  rewrite Hx, He, Hl; intuition.
-  Qed.
-
-  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
-  Proof.
-  intros x x' Hx l l' Hl. rewrite !In_alt.
-  setoid_rewrite Hl. setoid_rewrite Hx. intuition.
-  Qed.
-
-  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
-  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
-  Proof. intros l x x' H. rewrite H; auto. Qed.
-
-  Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
+  Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l.
   Proof. apply InfA_ltA; auto with *. Qed.
 
   Hint Immediate Inf_eq.
   Hint Resolve Inf_lt.
 
-  Lemma Sort_Inf_In :
-      forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
+  Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p.
   Proof. apply SortA_InfA_InA; auto with *. Qed.
 
-  Lemma Sort_Inf_NotIn :
-      forall l k e, Sort l -> Inf (k,e) l ->  ~In k l.
+  Lemma Sort_Inf_NotIn l k e : Sort l -> Inf (k,e) l ->  ~In k l.
   Proof.
     intros; red; intros.
     destruct H1 as [e' H2].
@@ -200,57 +122,34 @@ Module KeyOrderedType(Import O:OrderedType).
     repeat red; reflexivity.
   Qed.
 
-  Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
+  Lemma Sort_NoDupA l : Sort l -> NoDupA eqk l.
   Proof. apply SortA_NoDupA; auto with *. Qed.
 
-  Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
+  Lemma Sort_In_cons_1 l p q : Sort (p::l) -> InA eqk q l -> ltk p q.
   Proof.
    intros; invlist sort; eapply Sort_Inf_In; eauto.
   Qed.
 
-  Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
-      ltk e e' \/ eqk e e'.
+  Lemma Sort_In_cons_2 l p q : Sort (p::l) -> InA eqk q (p::l) ->
+      ltk p q \/ eqk p q.
   Proof.
     intros; invlist InA; auto with relations.
     left; apply Sort_In_cons_1 with l; auto with relations.
   Qed.
 
-  Lemma Sort_In_cons_3 :
-    forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.
+  Lemma Sort_In_cons_3 x l k e :
+    Sort ((k,e)::l) -> In x l -> ~O.eq x k.
   Proof.
     intros; invlist sort; red; intros.
     eapply Sort_Inf_NotIn; eauto using In_eq.
   Qed.
 
-  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
-  Proof.
-    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
-    right; exists x; auto.
-  Qed.
-
-  Lemma In_inv_2 : forall k k' e e' l,
-      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
-  Proof.
-   intros; invlist InA; intuition.
-  Qed.
-
-  Lemma In_inv_3 : forall x x' l,
-      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
-  Proof.
-   intros; invlist InA; compute in * |- ; intuition.
-  Qed.
-
  End Elt.
 
- Hint Unfold eqk eqke ltk.
- Hint Extern 2 (eqke ?a ?b) => split.
  Hint Resolve ltk_not_eqk ltk_not_eqke.
- Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
  Hint Immediate Inf_eq.
  Hint Resolve Inf_lt.
  Hint Resolve Sort_Inf_NotIn.
- Hint Resolve In_inv_2 In_inv_3.
 
 End KeyOrderedType.