cases hb with
| head => exact Mem.head _
| tail _ htail => exact Mem.tail _ (ih htail)
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ y :: reverseSpec ys
⊢ x ∈ y :: ys
no goals