You need to sign in or sign up before continuing.
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