From a666838951f9c53cd85c9d72474aa598ffe02a1e Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 24 Jul 2009 13:35:13 +0000
Subject: List: add a iff-based lemma about In and ++

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12249 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/List.v | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 34a9723475..7e9711bba5 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -316,7 +316,12 @@ Section Facts.
     now_show (H = a \/ In a (y ++ m)).
     elim H2; auto.
   Qed.
-  
+
+  Lemma in_app_iff : forall l l' (a:A), In a (l++l') <-> In a l \/ In a l'.
+  Proof.
+    split; auto using in_app_or, in_or_app.
+  Qed.
+
   Lemma app_inv_head:
    forall l l1 l2 : list A, l ++ l1 = l ++ l2 ->  l1 = l2.
   Proof.
@@ -1853,7 +1858,7 @@ End NatSeq.
   (** * Exporting hints and tactics *)
 
 
-Hint Rewrite 
+Hint Rewrite
   rev_involutive (* rev (rev l) = l *)
   rev_unit (* rev (l ++ a :: nil) = a :: rev l *)
   map_nth (* nth n (map f l) (f d) = f (nth n l d) *)
@@ -1861,9 +1866,6 @@ Hint Rewrite
   seq_length (* length (seq start len) = len *)
   app_length (* length (l ++ l') = length l + length l' *)
   rev_length (* length (rev l) = length l *)
-  : list.
-
-Hint Rewrite ->
   app_nil_r (* l ++ nil = l *)
   : list.
 
-- 
cgit v1.2.3