Commit 2022-04-12 03:21 955cb8e6
View on Github →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.
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.