case h
α : Type u_1
inst✝ : DecidableEq α
l a✝ : List α
⊢ l ∈ lists (Quotient.mk (isSetoid α) a✝) ↔ Quotient.mk (isSetoid α) a✝ = Quotient.mk (isSetoid α) l
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
l : List α
⊢ l ∈ lists s ↔ s = Quotient.mk (isSetoid α) l
induction s using Quotient.inductionOn
no goals
case h
α : Type u_1
inst✝ : DecidableEq α
l a✝ : List α
⊢ l ∈ lists (Quotient.mk (isSetoid α) a✝) ↔ Quotient.mk (isSetoid α) a✝ = Quotient.mk (isSetoid α) l
simpa using perm_comm