cases hlp
α : 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 cons
α : Type u
p : α → Prop
a : α
htail : List α
h_ind : List.forallr p htail → a ∈ htail → p a
a✝¹ : p a
a✝ : List.forallr p htail
⊢ p a