From 7736e153f134f873fba5683d97fa83378fb55f56 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 11 May 2006 21:42:15 +0000
Subject: decidabilite de InA

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

diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 726f569d60..47f632d65f 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
-- 
cgit v1.2.3