rw [←singleton_append, append_assoc]
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverse xs ++ x :: acc = reverse xs ++ [x] ++ acc
no goals