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