no goals
α : Type u
β : Type v
γ : Type w
a : α
as : List α
⊢ length (dropLast (a :: as)) = length as
match as with
| []       => rfl
| b::bs =>
  have ih := length_dropLast_cons b bs
  simp[dropLast, ih]
no goals
α : Type u
β : Type v
γ : Type w
a : α
as : List α
⊢ length (dropLast (a :: nil)) = length nil
rfl
α : Type u
β : Type v
γ : Type w
a : α
as : List α
b : α
bs : List α
ih : length (dropLast (b :: bs)) = length bs
⊢ length (dropLast (a :: b :: bs)) = length (b :: bs)
α : Type u
β : Type v
γ : Type w
a : α
as : List α
b : α
bs : List α
⊢ length (dropLast (a :: b :: bs)) = length (b :: bs)
have ih := length_dropLast_cons b bs
no goals
α : Type u
β : Type v
γ : Type w
a : α
as : List α
b : α
bs : List α
ih : length (dropLast (b :: bs)) = length bs
⊢ length (dropLast (a :: b :: bs)) = length (b :: bs)
simp[dropLast, ih]