Add lemmas about `last` and `head`: `last_app_or`, `head_app_or`, and `head_app`.

This MR adds lemmas about last and head: last_app_or, head_app_or, and head_app.