simp only [reverseSpec]
case mp.tail
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h_x_ys : Mem x ys
ih : x ∈ reverseSpec ys
⊢ x ∈ reverseSpec (y :: ys)
case mp.tail
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h_x_ys : Mem x ys
ih : x ∈ reverseSpec ys
⊢ x ∈ reverseSpec ys ++ [y]