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

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