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.

theories/fin_map_dom.v

@@ -198,6 +198,15 @@ Proof.
       naive_solver.
 Qed.
 
+Lemma dom_kmap `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2}
+    {A} (f : K → K2) `{!Inj (=) (=) f} (m : M A) :
+  dom D2 (kmap (M2:=M2) f m) ≡ set_map f (dom D m).
+Proof.
+  apply set_equiv. intros i.
+  rewrite !elem_of_dom, (lookup_kmap_is_Some _), elem_of_map.
+  by setoid_rewrite elem_of_dom.
+Qed.
+
 (** If [D] has Leibniz equality, we can show an even stronger result.  This is a
 common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
 (and thus also [gset K], the usual domain) but the value type [A] does not. *)
@@ -252,6 +261,11 @@ Section leibniz.
   Proof. unfold_leibniz. apply dom_union_inv. Qed.
 End leibniz.
 
+Lemma dom_kmap_L `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2}
+    `{!LeibnizEquiv D2} {A} (f : K → K2) `{!Inj (=) (=) f} (m : M A) :
+  dom D2 (kmap (M2:=M2) f m) = set_map f (dom D m).
+Proof. unfold_leibniz. by apply dom_kmap. Qed.
+
 (** * Set solver instances *)
 Global Instance set_unfold_dom_empty {A} i : SetUnfoldElemOf i (dom D (∅:M A)) False.
 Proof. constructor. by rewrite dom_empty, elem_of_empty. Qed.