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