theorem List.bw_law_1 {α : Type u_1} {xs : List α} [M : Monoid α] : foldr (fun (x1 x2 : α) => x1 * x2) 1 xs = foldl (fun (x1 x2 : α) => x1 * x2) 1 xs

theorem List.bw_law_2 {α : Type u_1} {xs : List α} {f g : α → α → α} {a : α} (h₁ : ∀ {x y z : α}, f x (g y z) = g (f x y) z) (h₂ : ∀ {x a : α}, f x a = g a x) : foldr f a xs = foldl g a xs

theorem List.bw_law_3 {α : Type u_1} {xs : List α} {f : α → α → α} {a : α} : foldr f a xs = foldl (flip f) a xs.reverse