diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index c8b7097abfeb12654258762ff0da3fc8ad580295..c955877ec89249d84865e842d6bf18a7575faf15 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -198,12 +198,12 @@ Proof.
       naive_solver.
 Qed.
 
-Lemma dom_map_kmap `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2}
+Lemma dom_kmap `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2}
     {A} (f : K → K2) `{!Inj (=) (=) f} (m : M A) :
-  dom D2 (map_kmap (M2:=M2) f m) ≡ set_map f (dom D m).
+  dom D2 (kmap (M2:=M2) f m) ≡ set_map f (dom D m).
 Proof.
   apply set_equiv. intros i.
-  rewrite !elem_of_dom, (lookup_map_kmap_is_Some _), elem_of_map.
+  rewrite !elem_of_dom, (lookup_kmap_is_Some _), elem_of_map.
   by setoid_rewrite elem_of_dom.
 Qed.
 
@@ -261,10 +261,10 @@ Section leibniz.
   Proof. unfold_leibniz. apply dom_union_inv. Qed.
 End leibniz.
 
-Lemma dom_map_kmap_L `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2}
+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 (map_kmap (M2:=M2) f m) = set_map f (dom D m).
-Proof. unfold_leibniz. by apply dom_map_kmap. Qed.
+  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.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 9bcc4934a64033d0d7fa0e550256d78aa2417f7e..e04532a17525d7317e847e8d3887a7492ea2c51d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -124,12 +124,12 @@ Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
     ∀ A, FinMapToList K A (M A)} {A B} (f : K → A → option B) (m : M A) : M B :=
   list_to_map (omap (λ ix, (fst ix ,.) <$> curry f ix) (map_to_list m)).
 
-(** Given a function [f : K1 → K2], the function [map_kmap f] turns a maps with
-keys of type [K1] into a map with keys of type [K2]. The function [map_kmap f]
+(** Given a function [f : K1 → K2], the function [kmap f] turns a maps with
+keys of type [K1] into a map with keys of type [K2]. The function [kmap f]
 is only well-behaved if [f] is injective, as otherwise it could map multiple
-entries into the same entry. All lemmas about [map_kmap f] thus have the premise
+entries into the same entry. All lemmas about [kmap f] thus have the premise
 [Inj (=) (=) f]. *)
-Definition map_kmap `{∀ A, Insert K2 A (M2 A), ∀ A, Empty (M2 A),
+Definition kmap `{∀ A, Insert K2 A (M2 A), ∀ A, Empty (M2 A),
     ∀ A, FinMapToList K1 A (M1 A)} {A} (f : K1 → K2) (m : M1 A) : M2 A :=
   list_to_map (fmap (prod_map f id) (map_to_list m)).
 
@@ -2533,13 +2533,13 @@ Section map_seq.
   Qed.
 End map_seq.
 
-Section map_kmap.
+Section kmap.
   Context `{FinMap K1 M1} `{FinMap K2 M2}.
   Context (f : K1 → K2) `{!Inj (=) (=) f}.
-  Local Notation map_kmap := (map_kmap (M1:=M1) (M2:=M2)).
+  Local Notation kmap := (kmap (M1:=M1) (M2:=M2)).
 
-  Lemma lookup_map_kmap_Some {A} (m : M1 A) (j : K2) x :
-    map_kmap f m !! j = Some x ↔ ∃ i, j = f i ∧ m !! i = Some x.
+  Lemma lookup_kmap_Some {A} (m : M1 A) (j : K2) x :
+    kmap f m !! j = Some x ↔ ∃ i, j = f i ∧ m !! i = Some x.
   Proof.
     assert (∀ x',
       (j, x) ∈ prod_map f id <$> map_to_list m →
@@ -2547,140 +2547,140 @@ Section map_kmap.
     { intros x'. rewrite !elem_of_list_fmap.
       intros [[j' y1] [??]] [[? y2] [??]]; simplify_eq/=.
       by apply (map_to_list_unique m j'). }
-    unfold map_kmap. rewrite <-elem_of_list_to_map', elem_of_list_fmap by done.
+    unfold kmap. rewrite <-elem_of_list_to_map', elem_of_list_fmap by done.
     setoid_rewrite elem_of_map_to_list'. split.
     - intros [[??] [??]]; naive_solver.
     - intros [? [??]]. eexists (_, _); naive_solver.
   Qed.
-  Lemma lookup_map_kmap_is_Some {A} (m : M1 A) (j : K2) :
-    is_Some (map_kmap f m !! j) ↔ ∃ i, j = f i ∧ is_Some (m !! i).
-  Proof. unfold is_Some. setoid_rewrite lookup_map_kmap_Some. naive_solver. Qed.
-  Lemma lookup_map_kmap_None {A} (m : M1 A) (j : K2) :
-    map_kmap f m !! j = None ↔ ∀ i, j = f i → m !! i = None.
+  Lemma lookup_kmap_is_Some {A} (m : M1 A) (j : K2) :
+    is_Some (kmap f m !! j) ↔ ∃ i, j = f i ∧ is_Some (m !! i).
+  Proof. unfold is_Some. setoid_rewrite lookup_kmap_Some. naive_solver. Qed.
+  Lemma lookup_kmap_None {A} (m : M1 A) (j : K2) :
+    kmap f m !! j = None ↔ ∀ i, j = f i → m !! i = None.
   Proof.
     setoid_rewrite eq_None_not_Some.
-    rewrite lookup_map_kmap_is_Some. naive_solver.
+    rewrite lookup_kmap_is_Some. naive_solver.
   Qed.
-  Lemma lookup_map_kmap {A} (m : M1 A) (i : K1) :
-    map_kmap f m !! f i = m !! i.
-  Proof. apply option_eq. setoid_rewrite lookup_map_kmap_Some. naive_solver. Qed.
-  Lemma lookup_total_map_kmap `{Inhabited A} (m : M1 A) (i : K1) :
-    map_kmap f m !!! f i = m !!! i.
-  Proof. by rewrite !lookup_total_alt, lookup_map_kmap. Qed.
+  Lemma lookup_kmap {A} (m : M1 A) (i : K1) :
+    kmap f m !! f i = m !! i.
+  Proof. apply option_eq. setoid_rewrite lookup_kmap_Some. naive_solver. Qed.
+  Lemma lookup_total_kmap `{Inhabited A} (m : M1 A) (i : K1) :
+    kmap f m !!! f i = m !!! i.
+  Proof. by rewrite !lookup_total_alt, lookup_kmap. Qed.
 
-  Global Instance map_kmap_inj {A} : Inj (=@{M1 A}) (=) (map_kmap f).
+  Global Instance kmap_inj {A} : Inj (=@{M1 A}) (=) (kmap f).
   Proof.
-    intros m1 m2 Hm. apply map_eq. intros i. by rewrite <-!lookup_map_kmap, Hm.
+    intros m1 m2 Hm. apply map_eq. intros i. by rewrite <-!lookup_kmap, Hm.
   Qed.
 
-  Lemma map_kmap_empty {A} : map_kmap f ∅ =@{M2 A} ∅.
-  Proof. unfold map_kmap. by rewrite map_to_list_empty. Qed.
-  Lemma map_kmap_empty_inv {A} (m : M1 A) : map_kmap f m = ∅ → m = ∅.
+  Lemma kmap_empty {A} : kmap f ∅ =@{M2 A} ∅.
+  Proof. unfold kmap. by rewrite map_to_list_empty. Qed.
+  Lemma kmap_empty_inv {A} (m : M1 A) : kmap f m = ∅ → m = ∅.
   Proof.
     intros Hm. apply map_empty; intros i.
-    apply (lookup_map_kmap_None _ (f i)); [|done]. by rewrite Hm, lookup_empty.
+    apply (lookup_kmap_None _ (f i)); [|done]. by rewrite Hm, lookup_empty.
   Qed.
 
-  Lemma map_kmap_singleton {A} i (x : A) : map_kmap f {[ i := x ]} = {[ f i := x ]}.
-  Proof. unfold map_kmap. by rewrite map_to_list_singleton. Qed.
+  Lemma kmap_singleton {A} i (x : A) : kmap f {[ i := x ]} = {[ f i := x ]}.
+  Proof. unfold kmap. by rewrite map_to_list_singleton. Qed.
 
-  Lemma map_kmap_partial_alter {A} (g : option A → option A) (m : M1 A) i :
-    map_kmap f (partial_alter g i m) = partial_alter g (f i) (map_kmap f m).
+  Lemma kmap_partial_alter {A} (g : option A → option A) (m : M1 A) i :
+    kmap f (partial_alter g i m) = partial_alter g (f i) (kmap f m).
   Proof.
     apply map_eq; intros j. apply option_eq; intros y.
     destruct (decide (j = f i)) as [->|?].
-    { by rewrite lookup_partial_alter, !lookup_map_kmap, lookup_partial_alter. }
-    rewrite lookup_partial_alter_ne, !lookup_map_kmap_Some by done. split.
+    { by rewrite lookup_partial_alter, !lookup_kmap, lookup_partial_alter. }
+    rewrite lookup_partial_alter_ne, !lookup_kmap_Some by done. split.
     - intros [i' [? Hm]]; simplify_eq/=.
       rewrite lookup_partial_alter_ne in Hm by naive_solver. naive_solver.
     - intros [i' [? Hm]]; simplify_eq/=. exists i'.
       rewrite lookup_partial_alter_ne by naive_solver. naive_solver.
   Qed.
-  Lemma map_kmap_insert {A} (m : M1 A) i x :
-    map_kmap f (<[i:=x]> m) = <[f i:=x]> (map_kmap f m).
-  Proof. apply map_kmap_partial_alter. Qed.
-  Lemma map_kmap_delete {A} (m : M1 A) i :
-    map_kmap f (delete i m) = delete (f i) (map_kmap f m).
-  Proof. apply map_kmap_partial_alter. Qed.
-  Lemma map_kmap_alter {A} (g : A → A) (m : M1 A) i :
-    map_kmap f (alter g i m) = alter g (f i) (map_kmap f m).
-  Proof. apply map_kmap_partial_alter. Qed.
-
-  Lemma map_kmap_merge {A B C} (g : option A → option B → option C)
+  Lemma kmap_insert {A} (m : M1 A) i x :
+    kmap f (<[i:=x]> m) = <[f i:=x]> (kmap f m).
+  Proof. apply kmap_partial_alter. Qed.
+  Lemma kmap_delete {A} (m : M1 A) i :
+    kmap f (delete i m) = delete (f i) (kmap f m).
+  Proof. apply kmap_partial_alter. Qed.
+  Lemma kmap_alter {A} (g : A → A) (m : M1 A) i :
+    kmap f (alter g i m) = alter g (f i) (kmap f m).
+  Proof. apply kmap_partial_alter. Qed.
+
+  Lemma kmap_merge {A B C} (g : option A → option B → option C)
       `{!DiagNone g} (m1 : M1 A) (m2 : M1 B) :
-    map_kmap f (merge g m1 m2) = merge g (map_kmap f m1) (map_kmap f m2).
+    kmap f (merge g m1 m2) = merge g (kmap f m1) (kmap f m2).
   Proof.
     apply map_eq; intros j. apply option_eq; intros y.
-    rewrite (lookup_merge g), lookup_map_kmap_Some.
+    rewrite (lookup_merge g), lookup_kmap_Some.
     setoid_rewrite (lookup_merge g). split.
-    { intros [i [-> ?]]. by rewrite !lookup_map_kmap. }
-    intros Hg. destruct (map_kmap f m1 !! j) as [x1|] eqn:Hm1.
-    { apply lookup_map_kmap_Some in Hm1 as (i&->&Hm1i).
-      exists i. split; [done|]. by rewrite Hm1i, <-lookup_map_kmap. }
-    destruct (map_kmap f m2 !! j) as [x2|] eqn:Hm2.
-    { apply lookup_map_kmap_Some in Hm2 as (i&->&Hm2i).
-      exists i. split; [done|]. by rewrite Hm2i, <-lookup_map_kmap, Hm1. }
+    { intros [i [-> ?]]. by rewrite !lookup_kmap. }
+    intros Hg. destruct (kmap f m1 !! j) as [x1|] eqn:Hm1.
+    { apply lookup_kmap_Some in Hm1 as (i&->&Hm1i).
+      exists i. split; [done|]. by rewrite Hm1i, <-lookup_kmap. }
+    destruct (kmap f m2 !! j) as [x2|] eqn:Hm2.
+    { apply lookup_kmap_Some in Hm2 as (i&->&Hm2i).
+      exists i. split; [done|]. by rewrite Hm2i, <-lookup_kmap, Hm1. }
     unfold DiagNone in *. naive_solver.
   Qed.
-  Lemma map_kmap_union_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
-    map_kmap f (union_with g m1 m2)
-    = union_with g (map_kmap f m1) (map_kmap f m2).
-  Proof. apply (map_kmap_merge _). Qed.
-  Lemma map_kmap_intersection_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
-    map_kmap f (intersection_with g m1 m2)
-    = intersection_with g (map_kmap f m1) (map_kmap f m2).
-  Proof. apply (map_kmap_merge _). Qed.
-  Lemma map_kmap_difference_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
-    map_kmap f (difference_with g m1 m2)
-    = difference_with g (map_kmap f m1) (map_kmap f m2).
-  Proof. apply (map_kmap_merge _). Qed.
-
-  Lemma map_kmap_union {A} (m1 m2 : M1 A) :
-    map_kmap f (m1 ∪ m2) = map_kmap f m1 ∪ map_kmap f m2.
-  Proof. apply map_kmap_union_with. Qed.
-  Lemma map_kmap_intersection {A} (m1 m2 : M1 A) :
-    map_kmap f (m1 ∩ m2) = map_kmap f m1 ∩ map_kmap f m2.
-  Proof. apply map_kmap_intersection_with. Qed.
-  Lemma map_kmap_difference {A} (m1 m2 : M1 A) :
-    map_kmap f (m1 ∖ m2) = map_kmap f m1 ∖ map_kmap f m2.
-  Proof. apply (map_kmap_merge _). Qed.
-
-  Lemma map_kmap_zip_with {A B C} (g : A → B → C) (m1 : M1 A) (m2 : M1 B) :
-    map_kmap f (map_zip_with g m1 m2) = map_zip_with g (map_kmap f m1) (map_kmap f m2).
-  Proof. by apply map_kmap_merge. Qed.
-
-  Lemma map_kmap_imap {A B} (g : K2 → A → option B) (m : M1 A) :
-    map_kmap f (map_imap (g ∘ f) m) = map_imap g (map_kmap f m).
+  Lemma kmap_union_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
+    kmap f (union_with g m1 m2)
+    = union_with g (kmap f m1) (kmap f m2).
+  Proof. apply (kmap_merge _). Qed.
+  Lemma kmap_intersection_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
+    kmap f (intersection_with g m1 m2)
+    = intersection_with g (kmap f m1) (kmap f m2).
+  Proof. apply (kmap_merge _). Qed.
+  Lemma kmap_difference_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
+    kmap f (difference_with g m1 m2)
+    = difference_with g (kmap f m1) (kmap f m2).
+  Proof. apply (kmap_merge _). Qed.
+
+  Lemma kmap_union {A} (m1 m2 : M1 A) :
+    kmap f (m1 ∪ m2) = kmap f m1 ∪ kmap f m2.
+  Proof. apply kmap_union_with. Qed.
+  Lemma kmap_intersection {A} (m1 m2 : M1 A) :
+    kmap f (m1 ∩ m2) = kmap f m1 ∩ kmap f m2.
+  Proof. apply kmap_intersection_with. Qed.
+  Lemma kmap_difference {A} (m1 m2 : M1 A) :
+    kmap f (m1 ∖ m2) = kmap f m1 ∖ kmap f m2.
+  Proof. apply (kmap_merge _). Qed.
+
+  Lemma kmap_zip_with {A B C} (g : A → B → C) (m1 : M1 A) (m2 : M1 B) :
+    kmap f (map_zip_with g m1 m2) = map_zip_with g (kmap f m1) (kmap f m2).
+  Proof. by apply kmap_merge. Qed.
+
+  Lemma kmap_imap {A B} (g : K2 → A → option B) (m : M1 A) :
+    kmap f (map_imap (g ∘ f) m) = map_imap g (kmap f m).
   Proof.
     apply map_eq; intros j. apply option_eq; intros y.
-    rewrite map_lookup_imap, bind_Some. setoid_rewrite lookup_map_kmap_Some.
+    rewrite map_lookup_imap, bind_Some. setoid_rewrite lookup_kmap_Some.
     setoid_rewrite map_lookup_imap. setoid_rewrite bind_Some. naive_solver.
   Qed.
-  Lemma map_kmap_omap {A B} (g : A → option B) (m : M1 A) :
-    map_kmap f (omap g m) = omap g (map_kmap f m).
+  Lemma kmap_omap {A B} (g : A → option B) (m : M1 A) :
+    kmap f (omap g m) = omap g (kmap f m).
   Proof.
     apply map_eq; intros j. apply option_eq; intros y.
-    rewrite lookup_omap, bind_Some. setoid_rewrite lookup_map_kmap_Some.
+    rewrite lookup_omap, bind_Some. setoid_rewrite lookup_kmap_Some.
     setoid_rewrite lookup_omap. setoid_rewrite bind_Some. naive_solver.
   Qed.
-  Lemma map_kmap_fmap {A B} (g : A → B) (m : M1 A) :
-    map_kmap f (g <$> m) = g <$> (map_kmap f m).
-  Proof. by rewrite !map_fmap_alt, map_kmap_omap. Qed.
+  Lemma kmap_fmap {A B} (g : A → B) (m : M1 A) :
+    kmap f (g <$> m) = g <$> (kmap f m).
+  Proof. by rewrite !map_fmap_alt, kmap_omap. Qed.
 
   Lemma map_disjoint_kmap {A} (m1 m2 : M1 A) :
-    map_kmap f m1 ##ₘ map_kmap f m2 ↔ m1 ##ₘ m2.
+    kmap f m1 ##ₘ kmap f m2 ↔ m1 ##ₘ m2.
   Proof.
-    rewrite !map_disjoint_spec. setoid_rewrite lookup_map_kmap_Some. naive_solver.
+    rewrite !map_disjoint_spec. setoid_rewrite lookup_kmap_Some. naive_solver.
   Qed.
   Lemma map_disjoint_subseteq {A} (m1 m2 : M1 A) :
-    map_kmap f m1 ⊆ map_kmap f m2 ↔ m1 ⊆ m2.
+    kmap f m1 ⊆ kmap f m2 ↔ m1 ⊆ m2.
   Proof.
-    rewrite !map_subseteq_spec. setoid_rewrite lookup_map_kmap_Some. naive_solver.
+    rewrite !map_subseteq_spec. setoid_rewrite lookup_kmap_Some. naive_solver.
   Qed.
   Lemma map_disjoint_subset {A} (m1 m2 : M1 A) :
-    map_kmap f m1 ⊂ map_kmap f m2 ↔ m1 ⊂ m2.
+    kmap f m1 ⊂ kmap f m2 ↔ m1 ⊂ m2.
   Proof. unfold strict. by rewrite !map_disjoint_subseteq. Qed.
-End map_kmap.
+End kmap.
 
 (** * Tactics *)
 (** The tactic [decompose_map_disjoint] simplifies occurrences of [disjoint]