∀ {α : Type u_1} {β : Type u_2} (op : β → β → β) [hc : Std.Commutative op] [ha : Std.Associative op] (b : β) (f : α → β)
  (s : Finset α), Finset.fold op b f s = Multiset.fold op b (Multiset.map f s.val)