Add function `map_kmap` that transforms the keys of a finite map.

This function map_kmap f allows one to turn maps with keys K1 (e.g., gmap K1 A) into maps with keys K2 (e.g., gmap K2 A), where f : K1 → K2.

Notes:

• The function f should be injective, otherwise map_kmap f is ill-behaved. Consider map_kmap (λ _, 0) {[ 0 := 10, 1 := 20 ]}. What's the result of that? Well, that depends on how the map is exactly represented (for gmap that depends on how exactly the Countable instances are defined).
• There are tons of generalizations of this function possible, e.g., with functions f that go to option K2 so that elements can be dropped, etc (similar to omap versus fmap), or that could also take the values into account (similar to imap versus fmap). I think the version in this MR is useful because it enjoys nice lemmas. Maybe in the future we could define a generic version and define the one in this MR in terms of a more generic version.
• Some of the lemmas hold without Inj (e.g. lookup_map_kmap_None). I don't think there's a point in doing that because then I can no longer use the generic lemmas about list_to_map, also map_kmap f where f is not injective is ill-behaved (as previously stated).

Thanks @jules for the suggestion and feedback.