proposition: Theorem fold_left_orb_true_in : forall (A : Type)(f : A -> bool)(ls : list A) a init, In a ls -> f a = true -> fold_left (fun b x => orb b (f x)) ls init = true.
proof: Proof. induction ls; intuition; simpl in *. intuition; subst. rewrite H0. rewrite orb_true_r. eapply fold_left_orb_true_init. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation