List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, ForallPairs, etc

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

4 files changed, 177 insertions, 140 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 1d4bb8f11..4c59971cb 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -1094,24 +1094,23 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   contradict Hnotin; rewrite <- Hnotin; exists e0; auto.
   Qed.
 
+  Hint Resolve NoDupA_eqk_eqke NoDupA_rev elements_3w : map.
+
   Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 ->
    eqA (fold f m1 i) (fold f m2 i).
   Proof.
   intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
-  apply fold_right_equivlistA_restr with
-    (R:=fun p p' => ~eqk p p') (eqA:=eqke) (eqB:=eqA); auto with *.
+  assert (NoDupA eqk (rev (elements m1))) by (auto with *).
+  assert (NoDupA eqk (rev (elements m2))) by (auto with *).
+  apply fold_right_equivlistA_restr with (R:=complement eqk)(eqA:=eqke);
+   auto with *.
   intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto.
-  unfold eq_key, eq_key_elt; repeat red. intuition eauto.
+  unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto.
   intros (k,e) (k',e'); unfold eq_key; simpl; auto.
-  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply ForallL2_equiv1 with (eqA:=eqk); try red ; unfold eq_key ; eauto with *.
-  apply NoDupA_rev; try red ; unfold eq_key; eauto with *. apply elements_3w.
-  red; intros.
-  rewrite 2 InA_rev by auto with *.
-  destruct x; rewrite <- 2 elements_mapsto_iff by auto with *.
-  rewrite 2 find_mapsto_iff by auto with *.
-  rewrite H. split; auto.
+  rewrite <- NoDupA_altdef; auto.
+  intros (k,e).
+  rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H;
+   auto with *.
   Qed.
 
   Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 ->
@@ -1121,33 +1120,27 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
   change (f k e (fold_right f' i (rev (elements m1))))
    with (f' (k,e) (fold_right f' i (rev (elements m1)))).
+  assert (NoDupA eqk (rev (elements m1))) by (auto with *).
+  assert (NoDupA eqk (rev (elements m2))) by (auto with *).
   apply fold_right_add_restr with
-    (R:=fun p p'=>~eqk p p')(eqA:=eqke)(eqB:=eqA); auto with *.
+   (R:=complement eqk)(eqA:=eqke)(eqB:=eqA); auto with *.
   intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. apply Comp; auto.
-
-  unfold eq_key_elt, eq_key; repeat red; intuition eauto.
+  unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto.
   unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto.
-  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply ForallL2_equiv1 with (eqA:=eqk); try red; unfold eq_key ; eauto with *.
-  apply NoDupA_rev; try red; eauto with *. apply elements_3w.
-  rewrite InA_rev; auto with *.
-  contradict H.
-  exists e.
-  rewrite elements_mapsto_iff; auto.
-  intros a.
-  destruct a as (a,b).
+  rewrite <- NoDupA_altdef; auto.
+  rewrite InA_rev, <- elements_mapsto_iff by (auto with *). firstorder.
+  intros (a,b).
   rewrite InA_cons, 2 InA_rev, <- 2 elements_mapsto_iff,
    2 find_mapsto_iff by (auto with *).
   unfold eq_key_elt; simpl.
   rewrite H0.
   rewrite add_o.
-  destruct (eq_dec k a); intuition.
-  inversion H1; auto.
-  f_equal; auto.
-  elim H.
-  exists b; apply MapsTo_1 with a; auto with map.
-  elim n; auto.
+  destruct (eq_dec k a) as [EQ|NEQ]; split; auto.
+  intros EQ'; inversion EQ'; auto.
+  intuition; subst; auto.
+  elim H. exists b; rewrite EQ; auto with map.
+  intuition.
+  elim NEQ; auto.
   Qed.
 
   Lemma fold_add : forall m k e i, ~In k m ->
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index b34bf65b3..f520c4fd6 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1838,40 +1838,96 @@ End NatSeq.
 
 (** * Existential and universal predicates over lists *)
 
-Inductive ExistsL {A} (P:A->Prop) : list A -> Prop :=
- | ExistsL_cons_hd : forall x l, P x -> ExistsL P (x::l)
- | ExistsL_cons_tl : forall x l, ExistsL P l -> ExistsL P (x::l).
-Hint Constructors ExistsL.
+Inductive Exists {A} (P:A->Prop) : list A -> Prop :=
+ | Exists_cons_hd : forall x l, P x -> Exists P (x::l)
+ | Exists_cons_tl : forall x l, Exists P l -> Exists P (x::l).
+Hint Constructors Exists.
 
-Lemma ExistsL_exists : forall A P (l:list A),
- ExistsL P l <-> (exists x, In x l /\ P x).
+Lemma Exists_exists : forall A P (l:list A),
+ Exists P l <-> (exists x, In x l /\ P x).
 Proof.
 split.
 induction 1; firstorder.
 induction l; firstorder; subst; auto.
 Qed.
 
-Lemma ExistsL_nil : forall A (P:A->Prop), ExistsL P nil <-> False.
+Lemma Exists_nil : forall A (P:A->Prop), Exists P nil <-> False.
 Proof. split; inversion 1. Qed.
 
-Lemma ExistsL_cons : forall A (P:A->Prop) x l,
- ExistsL P (x::l) <-> P x \/ ExistsL P l.
+Lemma Exists_cons : forall A (P:A->Prop) x l,
+ Exists P (x::l) <-> P x \/ Exists P l.
 Proof. split; inversion 1; auto. Qed.
 
 
-Inductive ForallL {A} (P:A->Prop) : list A -> Prop :=
- | ForallL_nil : ForallL P nil
- | ForallL_cons : forall x l, P x -> ForallL P l -> ForallL P (x::l).
-Hint Constructors ForallL.
+Inductive Forall {A} (P:A->Prop) : list A -> Prop :=
+ | Forall_nil : Forall P nil
+ | Forall_cons : forall x l, P x -> Forall P l -> Forall P (x::l).
+Hint Constructors Forall.
 
-Lemma ForallL_forall : forall A P (l:list A),
- ForallL P l <-> (forall x, In x l -> P x).
+Lemma Forall_forall : forall A P (l:list A),
+ Forall P l <-> (forall x, In x l -> P x).
 Proof.
 split.
 induction 1; firstorder; subst; auto.
 induction l; firstorder.
 Qed.
 
+(** [Forall2]: stating that elements of two lists are pairwise related. *)
+
+Inductive Forall2 {A B} (R:A->B->Prop) : list A -> list B -> Prop :=
+ | Forall2_nil : Forall2 R nil nil
+ | Forall2_cons : forall x y l l',
+    R x y -> Forall2 R l l' -> Forall2 R (x::l) (y::l').
+Hint Constructors Forall2.
+
+(** [ForallPairs] : specifies that a certain relation should
+    always hold when inspecting all possible pairs of elements of a list. *)
+
+Definition ForallPairs A (R : A -> A -> Prop) l :=
+ forall a b, In a l -> In b l -> R a b.
+
+(** [ForallOrdPairs] : we still check a relation over all pairs
+     of elements of a list, but now the order of elements matters. *)
+
+Inductive ForallOrdPairs A (R : A -> A -> Prop) : list A -> Prop :=
+  | FOP_nil : ForallOrdPairs R nil
+  | FOP_cons : forall a l,
+     Forall (R a) l -> ForallOrdPairs R l -> ForallOrdPairs R (a::l).
+Hint Constructors ForallOrdPairs.
+
+Lemma ForallOrdPairs_In : forall A (R:A->A->Prop) l,
+ ForallOrdPairs R l ->
+ forall x y, In x l -> In y l -> x=y \/ R x y \/ R y x.
+Proof.
+ induction 1.
+ inversion 1.
+ simpl; destruct 1; destruct 1; repeat subst; auto.
+ right; left. apply -> Forall_forall; eauto.
+ right; right. apply -> Forall_forall; eauto.
+Qed.
+
+
+(** [ForallPairs] implies [ForallOrdPairs]. The reverse implication is true
+    only when [R] is symmetric and reflexive. *)
+
+Lemma ForallPairs_ForallOrdPairs : forall A (R:A->A->Prop) l,
+ ForallPairs R l -> ForallOrdPairs R l.
+Proof.
+ induction l; auto. intros H.
+ constructor.
+ apply <- Forall_forall. intros; apply H; simpl; auto.
+ apply IHl. red; intros; apply H; simpl; auto.
+Qed.
+
+Lemma ForallOrdPairs_ForallPairs : forall A (R:A->A->Prop),
+ (forall x, R x x) ->
+ (forall x y, R x y -> R y x) ->
+ forall l, ForallOrdPairs R l -> ForallPairs R l.
+Proof.
+ intros A R Refl Sym l Hl x y Hx Hy.
+ destruct (ForallOrdPairs_In Hl _ _ Hx Hy); subst; intuition.
+Qed.
+
 
 (** * Inversion of predicates over lists based on head symbol *)
 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 8acb6a902..2aecb3fdb 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -33,10 +33,10 @@ Inductive InA (x : A) : list A -> Prop :=
 Hint Constructors InA.
 
 (** TODO: it would be nice to have a generic definition instead
-    of the previous one. Having [InA = ExistsL eqA] raises too
+    of the previous one. Having [InA = Exists eqA] raises too
     many compatibility issues. For now, we only state the equivalence: *)
 
-Lemma InA_altdef : forall x l, InA x l <-> ExistsL (eqA x) l.
+Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l.
 Proof. split; induction 1; auto. Qed.
 
 Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l.
@@ -53,7 +53,7 @@ Qed.
 
 Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l.
 Proof.
- intros; rewrite InA_altdef, ExistsL_exists; firstorder.
+ intros; rewrite InA_altdef, Exists_exists; firstorder.
 Qed.
 
 (** A list without redundancy modulo the equality over [A]. *)
@@ -64,11 +64,22 @@ Inductive NoDupA : list A -> Prop :=
 
 Hint Constructors NoDupA.
 
+(** An alternative definition of [NoDupA] based on [ForallOrdPairs] *)
+
+Lemma NoDupA_altdef : forall l,
+ NoDupA l <-> ForallOrdPairs (complement eqA) l.
+Proof.
+ split; induction 1; constructor; auto.
+ rewrite Forall_forall. intros b Hb.
+ intro Eq; elim H. rewrite InA_alt. exists b; auto.
+ rewrite InA_alt; intros (a' & Haa' & Ha').
+ rewrite Forall_forall in H. exact (H a' Ha' Haa').
+Qed.
 
-Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
 
 (** lists with same elements modulo [eqA] *)
 
+Definition inclA l l' := forall x, InA x l -> InA x l'.
 Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
 
 (** lists with same elements modulo [eqA] at the same place *)
@@ -80,6 +91,11 @@ Inductive eqlistA : list A -> list A -> Prop :=
 
 Hint Constructors eqlistA.
 
+(** We could also have written [eqlistA = Forall2 eqA]. *)
+
+Lemma eqlistA_altdef : forall l l', eqlistA l l' <-> Forall2 eqA l l'.
+Proof. split; induction 1; auto. Qed.
+
 (** Results concerning lists modulo [eqA] *)
 
 Hypothesis eqA_equiv : Equivalence eqA.
@@ -88,6 +104,8 @@ Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv).
 Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv).
 Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv).
 
+Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
+
 (** First, the two notions [equivlistA] and [eqlistA] are indeed equivlances *)
 
 Global Instance equivlist_equiv : Equivalence equivlistA.
@@ -292,108 +310,77 @@ induction 1; simpl; auto with relations.
 apply Comp; auto.
 Qed.
 
-(** [ForallL2] : specifies that a certain binary predicate should
-    always hold when inspecting two different elements of the list. *)
-
-Inductive ForallL2 (R : A -> A -> Prop) : list A -> Prop :=
-  | ForallNil : ForallL2 R nil
-  | ForallCons : forall a l,
-     (forall b, In b l -> R a b) ->
-     ForallL2 R l -> ForallL2 R (a::l).
-Hint Constructors ForallL2.
+(** Fold with restricted [transpose] hypothesis. *)
 
-(** [NoDupA] can be written in terms of [ForallL2] *)
-
-Lemma ForallL2_NoDupA : forall l,
- ForallL2 (fun a b => ~eqA a b) l <-> NoDupA l.
-Proof.
- induction l; split; intros; auto.
- invlist ForallL2. constructor; [ | rewrite <- IHl; auto ].
- rewrite InA_alt; intros (a',(Haa',Ha')).
- exact (H0 a' Ha' Haa').
- invlist NoDupA. constructor; [ | rewrite IHl; auto ].
- intros b Hb.
- contradict H0.
- rewrite InA_alt; exists b; auto.
-Qed.
+Section Fold_With_Restriction.
+Variable R : A -> A -> Prop.
+Hypothesis R_sym : Symmetric R.
+Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.
 
-Lemma ForallL2_impl : forall (R R':A->A->Prop),
- (forall a b, R a b -> R' a b) ->
- forall l, ForallL2 R l -> ForallL2 R' l.
-Proof.
- induction 2; auto.
-Qed.
 
-(** The following definition is easier to use than [ForallL2]. *)
+(*
 
-Definition ForallL2_alt (R:A->A->Prop) l :=
- forall a b, InA a l -> InA b l -> ~eqA a b -> R a b.
+(** [ForallOrdPairs R] is compatible with [equivlistA] over the
+    lists without duplicates, as long as the relation [R]
+    is symmetric and compatible with [eqA]. To prove this fact,
+    we use an auxiliary notion: "forall distinct pairs, ...".
+*)
 
-Section Restriction.
-Variable R : A -> A -> Prop.
+Definition ForallNeqPairs :=
+ ForallPairs (fun a b => ~eqA a b -> R a b).
 
-(** [ForallL2] and [ForallL2_alt] are related, but no completely
+(** [ForallOrdPairs] and [ForallNeqPairs] are related, but not completely
     equivalent. For proving one implication, we need to know that the
     list has no duplicated elements... *)
 
-Lemma ForallL2_equiv1 : forall l, NoDupA l ->
- ForallL2_alt R l -> ForallL2 R l.
+Lemma ForallNeqPairs_ForallOrdPairs : forall l, NoDupA l ->
+ ForallNeqPairs l -> ForallOrdPairs R l.
 Proof.
  induction l; auto.
- constructor. intros b Hb.
- inv.
- apply H0; auto.
+ constructor. inv.
+ rewrite Forall_forall; intros b Hb.
+ apply H0; simpl; auto.
  contradict H1; rewrite H1; auto.
  apply IHl.
  inv; auto.
  intros b c Hb Hc Hneq.
- apply H0; auto.
+ apply H0; simpl; auto.
 Qed.
 
 (** ... and for proving the other implication, we need to be able
-   to reverse and adapt relation [R] modulo [eqA]. *)
-
-Hypothesis R_sym : Symmetric R.
-Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.
+   to reverse relation [R]. *)
 
-Lemma ForallL2_equiv2 : forall l,
- ForallL2 R l -> ForallL2_alt R l.
+Lemma ForallOrdPairs_ForallNeqPairs : forall l,
+ ForallOrdPairs R l -> ForallNeqPairs l.
 Proof.
- induction l.
- intros _. red. intros a b Ha. inv.
- inversion_clear 1 as [|? ? H_R Hl].
- intros b c Hb Hc Hneq.
- inv.
- (* b,c = a : impossible *)
- elim Hneq; eauto.
- (* b = a, c in l *)
- rewrite InA_alt in H0; destruct H0 as (d,(Hcd,Hd)).
- rewrite H, Hcd; auto.
- (* b in l, c = a *)
- rewrite InA_alt in H; destruct H as (d,(Hcd,Hd)).
- rewrite H0, Hcd; auto.
- (* b,c in l *)
- apply (IHl Hl); auto.
+ intros l Hl x y Hx Hy N.
+ destruct (ForallOrdPairs_In Hl x y Hx Hy) as [H|[H|H]].
+ subst; elim N; auto.
+ assumption.
+ apply R_sym; assumption.
 Qed.
 
-Lemma ForallL2_equiv : forall l, NoDupA l ->
- (ForallL2 R l <-> ForallL2_alt R l).
-Proof.
-split; [apply ForallL2_equiv2|apply ForallL2_equiv1]; auto.
-Qed.
+*)
 
-Lemma ForallL2_equivlistA : forall l l', NoDupA l' ->
- equivlistA l l' -> ForallL2 R l -> ForallL2 R l'.
+(** Compatibility of [ForallOrdPairs] with respect to [inclA]. *)
+
+Lemma ForallOrdPairs_inclA : forall l l',
+ NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'.
 Proof.
-intros.
-apply ForallL2_equiv1; auto.
-intros a b Ha Hb Hneq.
-red in H0; rewrite <- H0 in Ha,Hb.
-revert a b Ha Hb Hneq.
-change (ForallL2_alt R l).
-apply ForallL2_equiv2; auto.
+induction l' as [|x l' IH].
+constructor.
+intros ND Incl FOP. apply FOP_cons; inv; unfold inclA in *; auto.
+rewrite Forall_forall; intros y Hy.
+assert (Ix : InA x (x::l')) by (rewrite InA_cons; auto).
+ apply Incl in Ix. rewrite InA_alt in Ix. destruct Ix as (x' & Hxx' & Hx').
+assert (Iy : InA y (x::l')) by (apply In_InA; simpl; auto).
+ apply Incl in Iy. rewrite InA_alt in Iy. destruct Iy as (y' & Hyy' & Hy').
+rewrite Hxx', Hyy'.
+destruct (ForallOrdPairs_In FOP x' y' Hx' Hy') as [E|[?|?]]; auto.
+absurd (InA x l'); auto. rewrite Hxx', E, <- Hyy'; auto.
 Qed.
 
+
 (** Two-argument functions that allow to reorder their arguments. *)
 Definition transpose (f : A -> B -> B) :=
   forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
@@ -405,7 +392,7 @@ Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
 Variable TraR :transpose_restr R f.
 
 Lemma fold_right_commutes_restr :
-  forall s1 s2 x, ForallL2 R (s1++x::s2) ->
+  forall s1 s2 x, ForallOrdPairs R (s1++x::s2) ->
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
 Proof.
 induction s1; simpl; auto; intros.
@@ -413,15 +400,15 @@ reflexivity.
 transitivity (f a (f x (fold_right f i (s1++s2)))).
 apply Comp; auto.
 apply IHs1.
-invlist ForallL2; auto.
+invlist ForallOrdPairs; auto.
 apply TraR.
-invlist ForallL2; auto.
-apply H0.
+invlist ForallOrdPairs; auto.
+rewrite Forall_forall in H0; apply H0.
 apply in_or_app; simpl; auto.
 Qed.
 
 Lemma fold_right_equivlistA_restr :
-  forall s s', NoDupA s -> NoDupA s' -> ForallL2 R s ->
+  forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
 Proof.
  simple induction s.
@@ -439,22 +426,23 @@ Proof.
  apply Hrec; auto.
  inv; auto.
  eapply NoDupA_split; eauto.
- invlist ForallL2; auto.
+ invlist ForallOrdPairs; auto.
  eapply equivlistA_NoDupA_split; eauto.
  transitivity (f y (fold_right f i (s1++s2))).
  apply Comp; auto. reflexivity.
  symmetry; apply fold_right_commutes_restr.
- apply ForallL2_equivlistA with (x::l); auto.
+ apply ForallOrdPairs_inclA with (x::l); auto.
+  red; intros; rewrite E; auto.
 Qed.
 
 Lemma fold_right_add_restr :
-  forall s' s x, NoDupA s -> NoDupA s' -> ForallL2 R s' -> ~ InA x s ->
+  forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
 Proof.
  intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto.
 Qed.
 
-End Restriction.
+End Fold_With_Restriction.
 
 (** we now state similar results, but without restriction on transpose. *)
 
@@ -475,7 +463,7 @@ Lemma fold_right_equivlistA :
 Proof.
 intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True);
  repeat red; auto.
-apply ForallL2_equiv1; try red; auto.
+apply ForallPairs_ForallOrdPairs; try red; auto.
 Qed.
 
 Lemma fold_right_add :
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index c72d3a79d..16da2162d 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -408,23 +408,23 @@ Module KeyOrderedType(Import O:OrderedType).
   exists e; auto.
   Qed.
 
-  Lemma In_alt2 : forall k l, In k l <-> ExistsL (fun p => eq k (fst p)) l.
+  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
   Proof.
   unfold In, MapsTo.
-  setoid_rewrite ExistsL_exists; setoid_rewrite InA_alt.
+  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 ExistsL_nil.
+  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, ExistsL_cons; intuition.
+  intros; rewrite !In_alt2, Exists_cons; intuition.
   Qed.
 
   Global Instance MapsTo_compat :