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