rw [reverseAux_spec]
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverseAux xs [x] = reverseSpec xs ++ [x]
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverse xs ++ [x] = reverseSpec xs ++ [x]