no goals
α : Type u_2
β : Type u_1
γ : Type ?u.25404
δ : Type ?u.25407
a : α
s t : Multiset α
f✝ g✝ f g : α → Multiset β
m : Multiset α
⊢ (∀ (a : α), a ∈ m → f a = g a) → bind m f = bind m g
simp (config := { contextual := true }) [bind]