rw [reverseAux_eq_append]
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) bs = reverse as₂ ++ reverseAux [] bs
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) [] ++ bs = reverse as₂ ++ reverseAux [] bs