diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2f4c088829901a0173a566376b444eb1c5877d4e..26ef6df1164c323f3639c570fbe2e43e4f600bda 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,17 @@ Coq 8.11 is no longer supported.
 - Declare `Hint Mode` for `FinSet A C` so that `C` is input, and `A` is output
   (i.e., inferred from `C`).
 - Add function `map_preimage` to compute the preimage of a finite map.
+- Rename `map_disjoint_subseteq` → `kmap_subseteq` and
+  `map_disjoint_subset` → `kmap_subset`.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bmap_disjoint_subseteq\b/kmap_subseteq/g
+s/\bmap_disjoint_subset\b/kmap_subset/g
+EOF
+```
 
 ## std++ 1.7.0 (2022-01-22)
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 720b154dd1a38f2487526c2fd977c7cfe01885b5..dc7cdc370eb2361f12ac5a9f81828c664f168053 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -3265,14 +3265,14 @@ Section kmap.
   Proof.
     rewrite !map_disjoint_spec. setoid_rewrite lookup_kmap_Some. naive_solver.
   Qed.
-  Lemma map_disjoint_subseteq {A} (m1 m2 : M1 A) :
+  Lemma kmap_subseteq {A} (m1 m2 : M1 A) :
     kmap f m1 ⊆ kmap f m2 ↔ m1 ⊆ m2.
   Proof.
     rewrite !map_subseteq_spec. setoid_rewrite lookup_kmap_Some. naive_solver.
   Qed.
-  Lemma map_disjoint_subset {A} (m1 m2 : M1 A) :
+  Lemma kmap_subset {A} (m1 m2 : M1 A) :
     kmap f m1 ⊂ kmap f m2 ↔ m1 ⊂ m2.
-  Proof. unfold strict. by rewrite !map_disjoint_subseteq. Qed.
+  Proof. unfold strict. by rewrite !kmap_subseteq. Qed.
 End kmap.
 
 Section preimage.