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
.
This MR adds lemmas about last
and head
: last_app_or
, head_app_or
, and head_app
.