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?
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?