proposition: Theorem ex_any_dec : forall (A : Type)(f : A -> bool)(ls : list A) a, In a ls -> f a = true -> any_dec f ls = true.
proof: Proof. unfold any_dec in *. induction ls; intuition idtac; simpl in *; intuition idtac; subst. rewrite H0. apply fold_left_orb_true. case_eq (f a); intros. apply fold_left_orb_true. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation