diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7af05c2cff77fa1125ecffa9bad6e460e9203d2d..3174c17381f9000a7c4e9956301706b8b9c0e2cb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -157,6 +157,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
     version `coreP_entails'` for `coreP P` with `P` affine.
   + Add instance `coreP_affine P : Affine P → Affine (coreP P)` and
     lemma `coreP_wand P Q : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q`.
+* Add lemma `mapsto_mapsto_ne : ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝`.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 091e77d61bd3579e529e8dd943a66855941ecbcc..afeaad2084af22e38e601201beb217ce9dfe97ad 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -233,6 +233,13 @@ Section gen_heap.
     iApply (mapsto_valid l _ v2). by iFrame.
   Qed.
 
+  Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
+    ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+  Proof.
+    iIntros (?) "Hl1 Hl2"; iIntros (->).
+    by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %?.
+  Qed.
+
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).
   Proof. rewrite meta_token_eq /meta_token_def. apply _. Qed.