match l with
| cancP :: t =>
match t with 
| [] =>  simp [p] at *
| h' :: t' =>
  simp [List.dropLast, List.getLast, split_drop]
α : Type
inst✝ : DecidableEq α
β : Type u_1
l : List β
p : l ≠ []
⊢ List.dropLast l ++ [List.getLast l p] = l
no goals