proposition: Theorem any_dec_ex : forall (A : Type)(f : A -> bool)(ls : list A), any_dec f ls = true -> exists a, In a ls /\ f a = true.
proof: Proof. unfold any_dec in *. induction ls; intuition idtac; simpl in *. discriminate. case_eq (f a); intros. econstructor. intuition idtac. rewrite H0 in H. edestruct IHls. trivial. intuition idtac. exists x. intuition idtac. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation