no goals
α : Type u
β : Type v
γ : Type w
as : List α
⊢ as ++ nil = as
induction as with
| nil => rfl
| cons a as ih =>
  simp_all [HAppend.hAppend, Append.append, List.append]
no goals
case nil
α : Type u
β : Type v
γ : Type w
⊢ nil ++ nil = nil
rfl
no goals
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
ih : as ++ nil = as
⊢ a :: as ++ nil = a :: as
simp_all [HAppend.hAppend, Append.append, List.append]