no goals
α : Type u
β : Type v
γ : Type w
as bs cs : List α
⊢ as ++ bs ++ cs = as ++ (bs ++ cs)
induction as with
| nil => rfl
| cons a as ih => simp [ih]
no goals
case nil
α : Type u
β : Type v
γ : Type w
bs cs : List α
⊢ nil ++ bs ++ cs = nil ++ (bs ++ cs)
rfl
no goals
case cons
α : Type u
β : Type v
γ : Type w
bs cs : List α
a : α
as : List α
ih : as ++ bs ++ cs = as ++ (bs ++ cs)
⊢ a :: as ++ bs ++ cs = a :: as ++ (bs ++ cs)
simp [ih]