Add map_agree
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