diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-02 18:51:43 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-02 18:51:43 +0000 |
| commit | b520fc53e0d4aba563ffc1cbdd480713b280fafc (patch) | |
| tree | 2d43fa1231cf338bdf941619c4b5ca0f6220af69 /theories/Structures | |
| parent | 0fb8601151a0e316554c95608de2ae4dbdac2ed3 (diff) | |
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
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrderedType2.v | 8 |
1 files changed, 4 insertions, 4 deletions
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 : |