case cons_mem
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l

case cons_duplicate
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l
α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
⊢ x ∈ l
cases' h with _ h _ _ h
no goals
case cons_mem
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l
exact h
no goals
case cons_duplicate
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l
exact h.mem