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.

added 1 commit

• 04383769 - Update CHANGELOG

Compare with previous version

added 4 commits

• 9c125edf - 1 commit from branch iris:master
• f592bbd8 - Add lemma `head_app`
• 0a372ddf - Add `last_app_or` and `head_app_or`
• 108d02ae - Update CHANGELOG

Compare with previous version

Thanks for the MR. The head_app makes perfect sense to me.

The _or lemmas seem to be a bit adhoc, especially since they only hold for → and not for ↔. What kind of a use case do you have in mind for them?

resolved all threads

added 1 commit

• ec7f3ffd - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

added 1 commit

• d0ac504d - Rewrite *_or lemmas

Compare with previous version

resolved all threads

added 1 commit

• a9a3ef7f - Update CHANGELOG.md

Compare with previous version

added 1 commit

• 587cd3d2 - Remove rogue '+' character

Compare with previous version

added 1 commit

• dc20a281 - Add *_None lemmas and use rewrite

Compare with previous version

resolved all threads

added 1 commit

• cec76a67 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

resolved all threads

added 1 commit

• 5b345f64 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version