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 α
hf : x ∈ xs
⊢ x ∈ reverseSpec xs
no goals