rw [cons_append, cons_append, ih, cons_append]
case cons
α : Type
as✝ bs cs : List α
a✝ b c a : α
as : List α
ih : as ++ bs ++ cs = as ++ (bs ++ cs)
⊢ a :: as ++ bs ++ cs = a :: as ++ (bs ++ cs)
no goals