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