Allow `map_imap` to be used in nested recursive fixpoints.

See the test file for an example.

I expect this change to be backwards compatible. Since the definition of map_imap is awful, I don't expect anyone to use it directly (i.e., perform unfold map_imap in proofs), but rather use map_lookup_imap or other lemmas.

added 2 commits

• e8ab345a - Test case.
• 3a077395 - CHANGELOG.

Compare with previous version

added 3 commits

• cff7852f - Allow `map_imap` to be used in nested recursive fixpoints.
• 1e56ec6a - Test case.
• cd35085f - CHANGELOG.

Compare with previous version

I also updated the comment. The complexity of both the old and new function is O (n log n), but I expect the new one to have slightly better constant factors since we no longer perform a conversion to list.

added 1 commit

• 3c517fd8 - Tweak comment.

Compare with previous version

resolved all threads

added 1 commit

• ce00f184 - Tweak comments and CHANGELOG.

Compare with previous version

enabled an automatic merge when the pipeline for ce00f184 succeeds

mentioned in commit 463bf9d8

merged