Add lemma `fmap_insert_inv`.

For other operations (empty, singleton) we have a similar lemma. This one is missing.

I had to move some things around in the file, and re-proved map_fmap_singleton_inv using the new lemma.