proposition: Theorem any_dec_app : forall (A : Type) f (ls1 ls2 : list A), any_dec f (ls1 ++ ls2) = any_dec f ls1 || any_dec f ls2.
proof: Proof. unfold any_dec in *. induction ls1; intuition idtac; simpl in *. case_eq (f a); intros. repeat rewrite fold_left_orb_true. trivial. eapply IHls1. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation