. intro hf
  induction hf with
  | head xs =>
    simp only [reverseSpec]
    apply mem_append_singleton
  | @tail y ys h_x_ys ih =>
    simp only [reverseSpec]
    apply mem_append_front _ _ _ ih
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
case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs