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).

CHANGELOG.md

@@ -119,7 +119,7 @@ longer supported by this release.
   tac` becomes `otac*`; the `feed` variants (that only specialize `→` but not
   `∀`) are no longer provided.
 - Add lemmas for `reverse` of `take`/`drop` and `take`/`drop` of `reverse`.
-- Rework lemmas for `take/drop` of an `++`:
+- 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