From 73e860125540855d8f9719c8f67d64cdb62b73fa Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 15 May 2006 08:42:53 +0000
Subject: petit ajout concernant InA

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8818 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/SetoidList.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 47f632d65f..dc9856bc0f 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -80,6 +80,17 @@ Proof.
 Qed.
 Hint Resolve In_InA.
 
+Lemma InA_split : forall l x, InA x l -> 
+ exists l1, exists y, exists l2, 
+ eqA x y /\ l = l1++y::l2.
+Proof.
+induction l; inversion_clear 1.
+exists (@nil A); exists a; exists l; auto.
+destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))).
+exists (a::l1); exists y; exists l2; auto.
+split; simpl; f_equal; auto.
+Qed.
+
 (** Results concerning lists modulo [eqA] and [ltA] *)
 
 Variable ltA : A -> A -> Prop.
-- 
cgit v1.2.3