proposition: Theorem any_dec_map : forall (A B : Type)(f1 : A -> B)(f2 : B -> bool)(ls : list A), any_dec (fun a => f2 (f1 a)) ls = any_dec f2 (map f1 ls).
proof: Proof. unfold any_dec in *. induction ls; intuition idtac; simpl in *. case_eq (f2 (f1 a)); intros. repeat rewrite fold_left_orb_true. trivial. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation