no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.37259
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ (bind 0 fun a => bind n fun b => f a b) = bind n fun b => bind 0 fun a => f a b
simp
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.37259
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((bind s fun a => bind n fun b => f a b) = bind n fun b => bind s fun a => f a b) →
      (bind (a ::ₘ s) fun a => bind n fun b => f a b) = bind n fun b => bind (a ::ₘ s) fun a => f a b
simp (config := { contextual := true })