Add map_Exists

Merged Michael Sammler requested to merge ci/msammler/map_Exists into master

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

Merge request reports