`zip_with_take_{l,r,both}{,'}` (was: Add lemma `zip_with_take_both`)

Merge it if you like it.

resolved all threads

added 1 commit

• 282d96fd - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

added 1 commit

• 4573b15f - specialize `zip_with_take_{l,r,both}` and generalize them into `zip_with_take_{l,r,both}'`

Compare with previous version

changed title from Add lemma zip_with_take_both to {+zip_with_take_{l,r,both}{,'} (was: +}Add lemma zip_with_take_both)

added 14 commits

• 4573b15f...77100af7 - 11 commits from branch iris:master
• 9869a4f8 - add lemma `zip_with_take_both`
• 3e75bfeb - specialize `zip_with_take_{l,r,both}` and generalize them into `zip_with_take_{l,r,both}'`
• d49329c7 - update changelog w.r.t. `zip_with_take_*` changes

Compare with previous version

resolved all threads

merged

mentioned in commit 78b6bc41

LGTM. Many thanks for implementing the suggested improvements!

@iris-users This MR changes some lemmas regarding zip_with and take:

• Add list.zip_with_take_both and list.zip_with_take_both'
• Specialize list.zip_with_take_{l,r}, add generalized lemmas list.zip_with_take_{l,r}'