α : Type u_2
β : Type u_1
γ : Type ?u.27686
δ : Type ?u.27689
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → HEq (f a) (f' a)
⊢ HEq (bind m f) (bind m f')
α : Type u_2
β : Type u_1
γ : Type ?u.27686
δ : Type ?u.27689
a : α
s t : Multiset α
f✝ g : α → Multiset β
β' : Type u_1
m : Multiset α
f : α → Multiset β
f' : α → Multiset β'
h : β = β'
hf : ∀ (a : α), a ∈ m → HEq (f a) (f' a)
⊢ HEq (bind m f) (bind m f')
subst h
α : Type u_2
β : Type u_1
γ : Type ?u.27686
δ : Type ?u.27689
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ HEq (bind m f) (bind m f')
α : Type u_2
β : Type u_1
γ : Type ?u.27686
δ : Type ?u.27689
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → HEq (f a) (f' a)
⊢ HEq (bind m f) (bind m f')
simp only [heq_eq_eq] at hf
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.27686
δ : Type ?u.27689
a : α
s t : Multiset α
f✝ g : α → Multiset β
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ HEq (bind m f) (bind m f')
simp [bind_congr hf]