proposition: Lemma exists_dec : forall (A : Type) (P : A -> Prop) (l : list A), (forall a, In a l -> {P a}+{~P a}) -> {a | In a l /\ P a}+{~exists a, In a l /\ P a}.
proof: Proof. intros A P l P_dec; induction l as [ | a l]. right; intros [a [a_in_nil _]]; absurd (In a nil); auto. destruct (P_dec a) as [Pa | not_Pa]. left; trivial. left; exists a; split; trivial; left; trivial. destruct IHl as [Ok | Ko]. intros; apply P_dec; right; trivial. destruct Ok as [b [b_in_l P_b]]. left; exists b; split; trivial; right; trivial. right; intros [b [[b_eq_a | b_in_l] Pb]]. subst; apply not_Pa; trivial. apply Ko; exists b; split; trivial. Defined.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)