diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3a7511d5dc660674c1a6e223730a7b95d28971fa..9e7a16e772d70a018bdb57ca2f6193f4fdf31486 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -29,13 +29,17 @@ Coq 8.11 is no longer supported.
 - Flip direction of `map_disjoint_fmap`.
 - Add `map_agree` as a weaker version of `##ₘ` which requires the maps to agree
   on keys contained in both maps. (by Michael Sammler)
+- Rename `lookup_union_l` → `lookup_union_l'` and add `lookup_union_l`
+  as the dual to `lookup_union_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`).
+Note that the script is not idempotent, do not run it twice.
 ```
 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
+s/\blookup_union_l\b/lookup_union_l'/g
 EOF
 ```
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 20a8857dc68f74a5b4a662ad3b1de6c5c9322f70..6331dde71f90e3031c41f1686f867b8c23347224 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2261,6 +2261,9 @@ Lemma lookup_union_r {A} (m1 m2 : M A) i :
   m1 !! i = None → (m1 ∪ m2) !! i = m2 !! i.
 Proof. intros Hi. by rewrite lookup_union, Hi, (left_id_L _ _).  Qed.
 Lemma lookup_union_l {A} (m1 m2 : M A) i :
+  m2 !! i = None → (m1 ∪ m2) !! i = m1 !! i.
+Proof. intros Hi. rewrite lookup_union, Hi. by destruct (m1 !! i). Qed.
+Lemma lookup_union_l' {A} (m1 m2 : M A) i :
   is_Some (m1 !! i) → (m1 ∪ m2) !! i = m1 !! i.
 Proof. intros [x Hi]. rewrite lookup_union, Hi. by destruct (m2 !! i). Qed.
 Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :