α : Type u_1
a : α
l : List α
h : a ∈ l
⊢ [a] <+ l
α : Type u_1
a : α
l : List α
⊢ [a] <+ l ↔ a ∈ l
refine ⟨fun h => h.subset (mem_singleton_self _), fun h => ?_⟩
case intro.intro
α : Type u_1
a : α
w✝¹ w✝ : List α
h : a ∈ w✝¹ ++ a :: w✝
⊢ [a] <+ w✝¹ ++ a :: w✝
α : Type u_1
a : α
l : List α
h : a ∈ l
⊢ [a] <+ l
obtain ⟨_, _, rfl⟩ := append_of_mem h
no goals
case intro.intro
α : Type u_1
a : α
w✝¹ w✝ : List α
h : a ∈ w✝¹ ++ a :: w✝
⊢ [a] <+ w✝¹ ++ a :: w✝
exact ((nil_sublist _).cons₂ _).trans (sublist_append_right ..)