diff options
| author | letouzey | 2006-05-15 08:42:53 +0000 |
|---|---|---|
| committer | letouzey | 2006-05-15 08:42:53 +0000 |
| commit | 73e860125540855d8f9719c8f67d64cdb62b73fa (patch) | |
| tree | 2726dc5186680ee98d6f804292edea41a9ca011c | |
| parent | 7152705f09c6280143d821e46e3bd57522a4a070 (diff) | |
petit ajout concernant InA
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8818 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Lists/SetoidList.v | 11 |
1 files changed, 11 insertions, 0 deletions
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. |