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