rw [List.concat_eq_append]
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ concat (dropLast as) (getLast as h) = as
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ dropLast as ++ [getLast as h] = as