induction l
α : Type u
p : α → Prop
l : List α
hlp : List.forallr p l
a : α
hMem : a ∈ l
⊢ p a
case nil
α : Type u
p : α → Prop
a : α
hlp : List.forallr p []
hMem : a ∈ []
⊢ p a

case cons
α : Type u
p : α → Prop
a head✝ : α
tail✝ : List α
tail_ih✝ : List.forallr p tail✝ → a ∈ tail✝ → p a
hlp : List.forallr p (head✝ :: tail✝)
hMem : a ∈ head✝ :: tail✝
⊢ p a