proposition: Theorem fold_left_orb_true : forall (A : Type)(f : A -> bool)(ls : list A), fold_left (fun b a => b || (f a)) ls true = true.
proof: Proof. induction ls; intuition idtac. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation