diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index efed8387ea57a950617af6781fabef9ea8e46f84..5de009c350ace8a10aa6817c20fb7abb8b2f77d6 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -232,6 +232,18 @@ Section tests.
   Qed.
 End tests.
 
+Section mapsto_tests.
+  Context `{!heapG Σ}.
+
+  (* Make sure certain tactic sequences can solve certain goals. *)
+  Lemma mapsto_combine l v :
+    l ↦{1/2} - ∗ l ↦{1/2} v -∗ l ↦ -.
+  Proof.
+    iIntros "[Hl1 Hl2]". iFrame. iExists _. done.
+  Qed.
+
+End mapsto_tests.
+
 Section inv_mapsto_tests.
   Context `{!heapG Σ}.
 
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 5cb0b05685e4be5b742e7cbcfee673669be313f3..c671e36a263c0d81e4587f477155fcae4dd57ea4 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,6 +1,7 @@
 From stdpp Require Import fin_maps.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
+From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
@@ -276,6 +277,17 @@ Qed.
 (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
 value type being [option val]. *)
 
+Global Instance ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
+Proof.
+  intros p q. iSplit.
+  - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
+  - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
+    iDestruct (mapsto_agree with "H1 H2") as %->. iExists v2. by iFrame.
+Qed.
+Global Instance ex_mapsto_as_fractional l q :
+  AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
+Proof. split. done. apply _. Qed.
+
 Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
 Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.