case cons_mem
α : Type u_1
l : List α
x : α
l' : List α
a✝ : x ∈ l'
⊢ x ∈ x :: l'

case cons_duplicate
α : Type u_1
l : List α
x y : α
l' : List α
a✝ : x ∈+ l'
hm : x ∈ l'
⊢ x ∈ y :: l'
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l
induction' h with l' _ y l' _ hm
no goals
case cons_mem
α : Type u_1
l : List α
x : α
l' : List α
a✝ : x ∈ l'
⊢ x ∈ x :: l'
exact mem_cons_self _ _
no goals
case cons_duplicate
α : Type u_1
l : List α
x y : α
l' : List α
a✝ : x ∈+ l'
hm : x ∈ l'
⊢ x ∈ y :: l'
exact mem_cons_of_mem _ hm