Folds over Boolean accumulation

A left fold that ors in a predicate computes any, from any starting accumulator. Candidate for Mathlib/Data/List/Basic.lean.

theorem List.foldl_or {α : Type u_1} (p : α → Bool) (acc : Bool) (l : List α) : foldl (fun (r : Bool) (a : α) => r || p a) acc l = (acc || l.any p)