diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index e2ff44a25570c050858a6d7964a6a71dc9a71d5d..a3b687feac18a16ca12a5c27d7c04f6ee160862f 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -204,6 +204,13 @@ Section gen_heap.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
+  Lemma mapsto_combine l q1 q2 v1 v2 :
+    l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ l ↦{q1 + q2} v1 ∗ ⌜v1 = v2⌝.
+  Proof.
+    iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
+    iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
+  Qed.
+
   Global Instance ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
   Proof.
     intros p q. iSplit.