rcases List.mem_cons.mp h with (h | h)
α : Type u
p : α → Prop
a a' : α
l : List α
h : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
⊢ p a'
case inl
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' = a
⊢ p a'

case inr
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' ∈ l
⊢ p a'