Theorem: Test.reverseAux_eq_append (Evaluation/FunctionalProgramming.lean)

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