diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-11 21:42:15 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-11 21:42:15 +0000 |
| commit | 7736e153f134f873fba5683d97fa83378fb55f56 (patch) | |
| tree | b92b138ef1b21251d262a7b27c94d9438a371f73 /theories/Lists/SetoidList.v | |
| parent | 9d0f4a0fdf6949a34105b53f24c55deec2f860ee (diff) | |
decidabilite de InA
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8807 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/SetoidList.v')
| -rw-r--r-- | theories/Lists/SetoidList.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 726f569d6..47f632d65 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -228,6 +228,18 @@ Section Remove. Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. +Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }. +Proof. +induction l. +right; auto. +red; inversion 1. +destruct (eqA_dec x a). +left; auto. +destruct IHl. +left; auto. +right; red; inversion_clear 1; tauto. +Qed. + Fixpoint removeA (x : A) (l : list A){struct l} : list A := match l with | nil => nil |