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