induction as generalizing bs with
| nil => rw [reverseAux, reverseAux]
| cons a as ih => rw [reverseAux, reverseAux, ←cons_append, ih]
α : Type
as bs cs : List α
a b c : α
⊢ reverseAux as (bs ++ cs) = reverseAux as bs ++ cs
no goals