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