induction as generalizing bs with
| nil => eggxplosion [reverseAux_nil, reverseAux_cons]
| cons a as ih =>
  eggxplosion [reverseAux_nil, reverseAux_cons, append_assoc]
α : Type u_1
as bs : List α
⊢ reverseAux as bs = reverseAux as [] ++ bs
no goals