no goals
α : Type u
β : Type v
γ : Type w
as : List α
a : α
⊢ length (concat as a) = length as + 1
induction as with
| nil => rfl
| cons _ xs ih => simp [concat, ih]
no goals
case nil
α : Type u
β : Type v
γ : Type w
a : α
⊢ length (concat nil a) = length nil + 1
rfl
no goals
case cons
α : Type u
β : Type v
γ : Type w
a head✝ : α
xs : List α
ih : length (concat xs a) = length xs + 1
⊢ length (concat (head✝ :: xs) a) = length (head✝ :: xs) + 1
simp [concat, ih]