diff --git a/CHANGELOG.md b/CHANGELOG.md
index 719bd427469e7570f050987ec2bae6e360b88e6c..a7e0ac0c06018eb9e1c6ec17828b5c3cd310b85f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -119,6 +119,12 @@ With this release, we dropped support for Coq 8.9.
   `big_sepL_dup`, `big_sepM_dup`, `big_sepS_dup`. Instead of having `□ (P -∗ P ∗
   P)` as an assumption these lemmas now assume `P` to be an instance of
   `Duplicable`.
+* Remove the `gen_heap` notations `l ↦ -` and `l ↦{q} -`. They were barely used
+  and looked very confusing in context: `l ↦ - ∗ P` looks like a magic wand.
+* Change `gen_inv_heap` notation `l ↦□ I` to `l ↦_I □`, so that `↦□` can be used
+  by `gen_heap`.
+* Strengthen `mapsto_valid_2` conclusion from `✓ (q1 + q2)%Qp` to
+  `⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝`.
 
 **Changes in `program_logic`:**
 
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 6d6caee52abf7a896d7098a5f9c21158113ccc13..634dae11f1cd52335262a2d89d19474b7747c6cb 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -126,10 +126,6 @@ Local Notation "l ↦{ q } v" := (mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
 Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
 
-Local Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
-  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
-Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
-
 Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_interp σ.
 Proof.
@@ -161,11 +157,23 @@ Section gen_heap.
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
   Proof. split. done. apply _. Qed.
 
+  Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
+  Proof.
+    rewrite mapsto_eq. iIntros "Hl".
+    iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
+  Qed.
+  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝.
+  Proof.
+    rewrite mapsto_eq. iIntros "H1 H2".
+    iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
+    eauto.
+  Qed.
+  (** Almost all the time, this is all you really need. *)
   Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
-    apply wand_intro_r.
-    rewrite mapsto_eq /mapsto_def -own_op own_valid discrete_valid.
-    apply pure_mono. intros [_ ?]%gmap_view_frag_op_valid_L. done.
+    iIntros "H1 H2".
+    iDestruct (mapsto_valid_2 with "H1 H2") as %[_ ?].
+    done.
   Qed.
 
   Lemma mapsto_combine l q1 q2 v1 v2 :
@@ -175,33 +183,11 @@ Section gen_heap.
     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.
-    - 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_valid l q v : l ↦{q} v -∗ ✓ q.
-  Proof.
-    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
-    rewrite gmap_view_frag_valid //.
-  Qed.
-  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ✓ (q1 + q2)%Qp.
-  Proof.
-    iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
-    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 %?.
+    by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
   Qed.
 
   (** General properties of [meta] and [meta_token] *)
diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index a43b372b53e36bdec9463843ba9e52e8566465ec..b180bb9b6c587e72f572004b41f879be332849dc 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -67,12 +67,12 @@ Section definitions.
 
 End definitions.
 
-Local Notation "l '↦□' I" := (inv_mapsto l I%stdpp%type)
-  (at level 20, format "l  '↦□'  I") : bi_scope.
-
 Local Notation "l '↦_' I v" := (inv_mapsto_own l v I%stdpp%type)
   (at level 20, I at level 9, format "l  '↦_' I  v") : bi_scope.
 
+Local Notation "l '↦_' I □" := (inv_mapsto l I%stdpp%type)
+  (at level 20, I at level 9, format "l  '↦_' I  '□'") : bi_scope.
+
 (* [inv_heap_inv] has no parameters to infer the types from, so we need to
    make them explicit. *)
 Arguments inv_heap_inv _ _ {_ _ _ _ _ _}.
@@ -133,7 +133,7 @@ Section inv_heap.
   (** * Helpers *)
 
   Lemma inv_mapsto_lookup_Some l h I :
-    l ↦□ I -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
+    l ↦_I □ -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
     ⌜∃ v I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
   Proof.
     iIntros "Hl_inv Hâ—¯".
@@ -179,10 +179,10 @@ Section inv_heap.
   Global Instance inv_heap_inv_persistent : Persistent (inv_heap_inv L V).
   Proof. apply _. Qed.
 
-  Global Instance inv_mapsto_persistent l I : Persistent (l ↦□ I).
+  Global Instance inv_mapsto_persistent l I : Persistent (l ↦_I □).
   Proof. apply _. Qed.
 
-  Global Instance inv_mapsto_timeless l I : Timeless (l ↦□ I).
+  Global Instance inv_mapsto_timeless l I : Timeless (l ↦_I □).
   Proof. apply _. Qed.
 
   Global Instance inv_mapsto_own_timeless l v I : Timeless (l ↦_I v).
@@ -201,7 +201,7 @@ Section inv_heap.
     destruct (h !! l) as [v'| ] eqn: Hlookup.
     - (* auth map contains l --> contradiction *)
       iDestruct (big_sepM_lookup with "HsepM") as "[_ Hl']"; first done.
-      by iDestruct (mapsto_valid_2 with "Hl Hl'") as %?.
+      by iDestruct (mapsto_valid_2 with "Hl Hl'") as %[??].
     - iMod (own_update with "H●") as "[H● H◯]".
       { apply lookup_to_inv_heap_None in Hlookup.
         apply (auth_update_alloc _
@@ -215,7 +215,7 @@ Section inv_heap.
       + iModIntro. by rewrite /inv_mapsto_own to_inv_heap_singleton.
   Qed.
 
-  Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦□ I.
+  Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦_I □.
   Proof.
     apply own_mono, auth_frag_mono. rewrite singleton_included pair_included.
     right. split; [apply: ucmra_unit_least|done].
@@ -266,7 +266,7 @@ Section inv_heap.
 
   Lemma inv_mapsto_acc l I E :
     ↑inv_heapN ⊆ E →
-    inv_heap_inv L V -∗ l ↦□ I ={E, E ∖ ↑inv_heapN}=∗
+    inv_heap_inv L V -∗ l ↦_I □ ={E, E ∖ ↑inv_heapN}=∗
     ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
   Proof.
     iIntros (HN) "#Hinv Hl_inv".
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 84cf1e7abb166528481a4e331bcc971e66231e4b..2de2bcbcf2dba9f7fd16c112b7a6bf8c35cb0ce7 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -291,6 +291,12 @@ Global Instance ex_mapsto_as_fractional l q :
   AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
 Proof. split. done. apply _. Qed.
 
+Lemma mapsto_valid_2 l q1 q2 v1 v2 :
+  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝.
+Proof.
+  iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
+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.
 
@@ -303,8 +309,6 @@ Qed.
 
 Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
 Proof. apply mapsto_valid. Qed.
-Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ✓ (q1 + q2)%Qp.
-Proof. apply mapsto_valid_2. Qed.
 Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
   ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_mapsto_ne. Qed.