Add map_agree

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

As discussed with @robbertkrebbers. I am not sure if there are good lemmas for insert and union of map_agree (i.e. corresponding to map_disjoint_union_l and map_disjoint_insert_l). Do you have ideas for how they would look like?

Edited by Michael Sammler

Merge request reports