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