no goals
α : Type u
β : Type v
γ : Type w
as bs : List α
⊢ length (as ++ bs) = length as + length bs
induction as with
| nil => simp
| cons _ as ih => simp [ih, Nat.succ_add]
no goals
case nil
α : Type u
β : Type v
γ : Type w
bs : List α
⊢ length (nil ++ bs) = length nil + length bs
simp
no goals
case cons
α : Type u
β : Type v
γ : Type w
bs : List α
head✝ : α
as : List α
ih : length (as ++ bs) = length as + length bs
⊢ length (head✝ :: as ++ bs) = length (head✝ :: as) + length bs
simp [ih, Nat.succ_add]