proposition: Lemma list_exists_is_sound : forall (A : Type) (f : A -> bool) (l : list A), list_exists f l = true <-> (exists a, In a l /\ f a = true).
proof: Proof. intros A f l; induction l as [ | a l]; simpl. split; [intros; discriminate | intros [a [Abs _]]; contradiction]. assert (H: forall a', a' = a -> f a' = f a). intros; subst; trivial. destruct (f a); simpl; generalize (H _ (eq_refl _)); clear H; intro H; split; intro H'. exists a; split; trivial; left; trivial. trivial. destruct ((proj1 IHl) H') as [a' [a'_in_l fa']]; exists a'; split; trivial; right; trivial. destruct H' as [a' [[a_eq_a' | a'_in_l] fa']]. subst a'; rewrite H in fa'; absurd (false = true); trivial; discriminate. apply (proj2 IHl); exists a'; split; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)