Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`.

• Add lemma map_omap_union.
• Add lemmas map_disjoint_fmap and map_disjoint_omap.
• Add lemmas fmap_merge and omap_merge.
• Add lemma omap_delete.
• Generalize 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.
• Generalize map_size_insert and map_size_delete in the same way.
• Add lemmas lookup_fmap_Some, lookup_omap_Some, and lookup_omap_id_Some.