basic): add a theorem about last and append (#13336)

Commit

3 years ago

feat(data/list/basic): add a theorem about last and append (#13336) When `ys` is not empty, we can conclude that `last (xs ++ ys)` is `last ys`.

Author

sorawee

Parents