intro a
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
⊢ l.toFinset ⊆ l'.toFinset
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
⊢ a ∈ l.toFinset → a ∈ l'.toFinset