simp only [reverse, reverseAux]
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverseAux (x :: xs) acc = reverse (x :: xs) ++ acc
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverseAux xs (x :: acc) = reverseAux xs [x] ++ acc