simp only [HAppend.hAppend, Append.append, List.append] at hb
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ [y] ++ reverseSpec ys
⊢ x ∈ y :: ys
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ y :: reverseSpec ys
⊢ x ∈ y :: ys