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