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

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