no goals
ι : Type ?u.159176
α : Type u_1
β : Type ?u.159182
γ : Type ?u.159185
s : Multiset α
⊢ sum (map (fun a => {a}) 0) = 0
simp
no goals
ι : Type ?u.159176
α : Type u_1
β : Type ?u.159182
γ : Type ?u.159185
s : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α}, sum (map (fun a => {a}) s) = s → sum (map (fun a => {a}) (a ::ₘ s)) = a ::ₘ s
simp