no goals
α : Type u_1
β : Type ?u.478700
γ : Type ?u.478703
r : α → α → Prop
s t : Multiset α
hst : Rel r s t
a✝ b✝ : α
as✝ bs✝ : Multiset α
hab : r a✝ b✝
_hst : Rel r as✝ bs✝
ih : map (Quot.mk r) as✝ = map (Quot.mk r) bs✝
⊢ map (Quot.mk r) (a✝ ::ₘ as✝) = map (Quot.mk r) (b✝ ::ₘ bs✝)
simp [ih, Quot.sound hab]