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