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