cases hMem
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
hMem : a ∈ hhead :: htail
⊢ p a
case head
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (a :: htail)
⊢ p a

case tail
α : Type u
p : α → Prop
a hhead : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
hlp : List.forallr p (hhead :: htail)
a✝ : Mem a htail
⊢ p a