no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
inst✝ : DecidableEq α✝
α : Type u_1
l : List α
a : α
x✝ : [a] <+~ l
s : List α
hla : s ~ [a]
h : s <+ l
⊢ a ∈ l
rwa [perm_singleton.mp hla, singleton_sublist] at h