rw [as.dropLast_eq_take, as.singleton_getLast_eq_drop]
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ dropLast as ++ [getLast as h] = as
α : Type u
β : Type v
γ : Type w
as : List α
h : as ≠ []
⊢ take (length as - 1) as ++ drop (length as - 1) as = as