map_omap_union.map_disjoint_fmap and map_disjoint_omap.fmap_merge and omap_merge.omap_delete.omap_insert and omap_singleton to cover both the Some and None case. Add _Some and _None versions of the lemmas for the specific cases.map_size_insert and map_size_delete in the same way.lookup_fmap_Some, lookup_omap_Some, and lookup_omap_id_Some.