proposition: Theorem any_dec_cons : forall (A : Type)(f : A -> bool)(ls : list A)(a : A), any_dec f (a :: ls) = f a || any_dec f ls.
proof: Proof. intuition idtac. unfold any_dec. simpl. case_eq (f a); intros. rewrite fold_left_orb_true. trivial. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation