apply Iff.intro
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs ↔ x ∈ reverseSpec xs
case mp
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs → x ∈ reverseSpec xs

case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs