simp only [reverseSpec] at hb
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ reverseSpec (y :: ys)
⊢ x ∈ y :: ys
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ reverseSpec ys ++ [y]
⊢ x ∈ y :: ys