induction xs generalizing acc with
| nil => simp [reverse, reverseAux]
| cons x xs ih =>
  simp only [reverse, reverseAux]
  simp only [ih]
  rw [←singleton_append, append_assoc]
α : Type u_1
xs acc : List α
⊢ reverseAux xs acc = reverse xs ++ acc
no goals