diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2d590c0175a64443e824c2b0936ee785fd313dd4..80dd8afdbfb8776c8a579a843c87bde2b2be522e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -116,6 +116,9 @@ API-breaking change is listed.
 - Swap names of `curry`/`uncurry`, `curry3`/`uncurry3`, `curry4`/`uncurry4`,
   `gmap_curry`/`gmap_uncurry`, and `hcurry`/`huncurry` to be consistent with
   Haskell and friends.
+- Rename `map_union_subseteq_l_alt` → `map_union_subseteq_l'` and
+  `map_union_subseteq_r_alt` → `map_union_subseteq_r'` to be consistent with
+  `or_intro_{l,r}'`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -156,6 +159,8 @@ s/\bgmap_uncurry_non_empty\b/gmap_curry_non_empty/g
 s/\bgmap_uncurry_curry_non_empty\b/gmap_curry_uncurry_non_empty/g
 s/\bhcurry_uncurry\b/huncurry_curry/g
 s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g
+# map_union_subseteq
+s/\bmap_union_subseteq_(r|l)_alt\b/map_union_subseteq_\1'/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 920b94265c5e930bb11c9ff071b2f6b8ff3532b5..9c8ff8b9b7f09fb4797b8c09999f27ce02849efc 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2039,9 +2039,9 @@ Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ##ₘ m2 → m2 ⊆ m1 ∪ m2.
 Proof.
   intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
 Qed.
-Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
+Lemma map_union_subseteq_l' {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
 Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
-Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
+Lemma map_union_subseteq_r' {A} (m1 m2 m3 : M A) :
   m2 ##ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3.
 Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
 Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2.