Add map_Exists

As discussed with @robbertkrebbers. I proved most of the lemmas corresponding to map_Forall.

assigned to @msammler

I proved most of the lemmas corresponding to map_Forall.

Just checking since you write "most", which ones are missing? Are they missing because they are false, or you don't have time to port them?

added 1 commit

• 1d4e7246 - Add map_Exists

Compare with previous version

unassigned @msammler

added 2 commits

• b1447a1b - Add `map_Exists_lookup_{1,2}`.
• 98c325cc - Add `map_Exists_ind`.

Compare with previous version

LGTM. Can you add a CHANGELOG?

added 9 commits

• 98c325cc...224790c8 - 6 commits from branch master
• 183bc449 - Add map_Exists
• ff92006d - Add `map_Exists_lookup_{1,2}`.
• 457abb83 - Add `map_Exists_ind`.

Compare with previous version

added 1 commit

• e68a2684 - Add CHANGELOG for `map_Exists`

Compare with previous version

resolved all threads

added 1 commit

• 3ebfb878 - Add CHANGELOG for `map_Exists`

Compare with previous version

resolved all threads

enabled an automatic merge when the pipeline for 3ebfb878 succeeds

merged

mentioned in commit ba7cf37b