no goals
α : Type u_1
β : Type ?u.444282
γ : Type ?u.444285
inst✝ : DecidableEq α
s t l l' : Multiset α
hl : Nodup l
hl' : Nodup l'
h : toFinset l = toFinset l'
⊢ l = l'
simpa [← toFinset_eq hl, ← toFinset_eq hl'] using h