ι : Type ?u.44810
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
l : List α
h : l ≠ []
h' : head! l ∈ head! l :: tail l
⊢ head! l ∈ l
ι : Type ?u.44810
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
l : List α
h : l ≠ []
⊢ head! l ∈ l
have h' := mem_cons_self l.head! l.tail
no goals
ι : Type ?u.44810
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
l : List α
h : l ≠ []
h' : head! l ∈ head! l :: tail l
⊢ head! l ∈ l
rwa [cons_head!_tail h] at h'