no goals
α : Type u_1
β : Type ?u.69645
γ : Type ?u.69648
δ : Type ?u.69651
σ : α → Type u_2
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ Multiset.sigma (a ::ₘ s) t = map (Sigma.mk a) (t a) + Multiset.sigma s t
simp [Multiset.sigma]