no goals
α : Type u_1
β : Type ?u.6065
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op b a) s
rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]