Rework lemmas for `take/drop` of an `++`:

• Add take_app and drop_app, which are the strongest versions, and use take_app_X for derived versions.
• Consistently use ' suffix for version with premise n = length, and have versions without ' with length inlined.
• Rename take_app → take_app_length, take_app_alt → take_app_length', take_add_app → take_app_add', take_app3_alt → take_app3_length', drop_app → drop_app_length, drop_app_alt → drop_app_length', drop_add_app → drop_app_add', drop_app3_alt → drop_app3_length'.

This closes #197 (closed).

mentioned in issue #197 (closed)

LGTM modulo the nit; feel free to merge whenever you have time to fix the reverse dependencies.

resolved all threads

added 1 commit

• 0f3cc9f7 - CHANGELOG tweak.

Compare with previous version

added 6 commits

• 0f3cc9f7...0de86dec - 3 commits from branch master
• a390c805 - Make `take`/`drop` lemmas for `app` more uniform.
• 4ece5004 - CHANGELOG.
• ffdc7802 - CHANGELOG tweak.

Compare with previous version

enabled an automatic merge when the pipeline for ffdc7802 succeeds

@iris-users Rework lemmas for take/drop of an ++:

• Add take_app and drop_app, which are the strongest versions, and use take_app_X for derived versions.
• Consistently use ' suffix for version with premise n = length, and have versions without ' with length inlined.
• Rename take_app → take_app_length, take_app_alt → take_app_length', take_add_app → take_app_add', take_app3_alt → take_app3_length', drop_app → drop_app_length, drop_app_alt → drop_app_length', drop_add_app → drop_app_add', drop_app3_alt → drop_app3_length'.

See the CHANGELOG for a sed script.

merged

mentioned in commit c57a2eed