case cons hhead htail h_ind =>
  cases hMem
  case head => cases hlp; assumption
  case tail hMem => apply h_ind ?_ hMem; cases hlp; assumption
α : 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
no goals