See the test file for an example.
I expect this change to be backwards compatible. Since the definition of map_imap is awful, I don't expect anyone to use it directly (i.e., perform unfold map_imap in proofs), but rather use map_lookup_imap or other lemmas.