diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 755f2d4ef778d568a55ce516e98530f7a98443ae..d3b668f05421b282a875a53d997ccb7d1f3b983b 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -32,13 +32,6 @@ Inductive dfrac :=
   | DfracDiscarded : dfrac
   | DfracBoth : Qp → dfrac.
 
-Declare Scope dfrac_scope.
-Delimit Scope dfrac_scope with dfrac.
-
-Notation "# q" := (DfracOwn q%Qp) (at level 8, format "# q") : dfrac_scope.
-Notation "#â–¡" := (DfracDiscarded) : dfrac_scope.
-Notation "â–¡" := (DfracDiscarded) : dfrac_scope.
-
 Section dfrac.
   Canonical Structure dfracO := leibnizO dfrac.
 
@@ -168,6 +161,16 @@ Section dfrac.
   Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
 
+  Lemma dfrac_valid_own_r dq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
+  Proof.
+    destruct dq as [q'| |q']; [|done|].
+    - apply Qp_lt_le_trans, Qp_lt_add_r.
+    - intro Hlt. etrans; last apply Hlt. apply Qp_lt_add_r.
+  Qed.
+
+  Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
+  Proof. rewrite comm. apply dfrac_valid_own_r. Qed.
+
   Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
   Proof. done. Qed.
 
@@ -181,12 +184,11 @@ Section dfrac.
   Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.
 
   (** Discarding a fraction is a frame preserving update. *)
-  Lemma dfrac_discard_update q : DfracOwn q ~~> DfracDiscarded.
+  Lemma dfrac_discard_update dq : dq ~~> DfracDiscarded.
   Proof.
-    intros n [[q'| |q']|];
-      rewrite /op /cmra_op -!cmra_discrete_valid_iff /valid /cmra_valid //=.
-    - intros. apply Qp_lt_le_trans with (q + q')%Qp; [|done]. apply Qp_lt_add_r.
-    - intros. apply Qp_le_lt_trans with (q + q')%Qp; [|done]. apply Qp_le_add_r.
+    intros n [[q'| |q']|]; rewrite -!cmra_discrete_valid_iff //=.
+    - apply dfrac_valid_own_r.
+    - apply cmra_valid_op_r.
   Qed.
 
 End dfrac.
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index a70dd4db1e05963492d8dde6416a97e67d916a75..137e1cd55d72af58f5296b6474dc6ac481d0847a 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -378,13 +378,13 @@ Section lemmas.
       rewrite lookup_insert_ne //.
   Qed.
 
-  Lemma gmap_view_persist k q v :
-    gmap_view_frag k (DfracOwn q) v ~~> gmap_view_frag k DfracDiscarded v.
+  Lemma gmap_view_persist k dq v :
+    gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
   Proof.
     apply view_update_frag=>m n bf Hrel j [df va] /=.
     rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
     - rewrite lookup_singleton.
-      edestruct (Hrel k ((DfracOwn q, to_agree v) â‹…? bf !! k)) as (v' & Hdf & Hva & Hm).
+      edestruct (Hrel k ((dq, to_agree v) â‹…? bf !! k)) as (v' & Hdf & Hva & Hm).
       { rewrite lookup_op lookup_singleton.
         destruct (bf !! k) eqn:Hbf; by rewrite Hbf. }
       rewrite Some_op_opM. intros [= Hbf].
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index b1ec17e94e365f278b8facf6cd080b4ec0d0abd1..5df0215f54c6ac439cb1b54c50dc5cfe6e8f2a5a 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
 Import uPred.
 
 (** This file provides a generic mechanism for a language-level point-to
-connective [l ↦{q} v] reflecting the physical heap.  This library is designed to
+connective [l ↦{dq} v] reflecting the physical heap.  This library is designed to
 be used as a singleton (i.e., with only a single instance existing in any
 proof), with the [gen_heapG] typeclass providing the ghost names of that unique
 instance.  That way, [mapsto] does not need an explicit [gname] parameter.
@@ -21,7 +21,7 @@ physical state, you will likely want explicit ghost names and are thus better
 off using [algebra.lib.gmap_view] together with [base_logic.lib.own].
 
 This library is generic in the types [L] for locations and [V] for values and
-supports fractional permissions.  Next to the point-to connective [l ↦{q} v],
+supports fractional permissions.  Next to the point-to connective [l ↦{dq} v],
 which keeps track of the value [v] of a location [l], this library also provides
 a way to attach "meta" or "ghost" data to locations. This is done as follows:
 
@@ -101,8 +101,8 @@ Section definitions.
     own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO V))) ∗
     own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L gnameO)).
 
-  Definition mapsto_def (l : L) (q : dfrac) (v: V) : iProp Σ :=
-    own (gen_heap_name hG) (gmap_view_frag l q (v : leibnizO V)).
+  Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
+    own (gen_heap_name hG) (gmap_view_frag l dq (v : leibnizO V)).
   Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
   Definition mapsto := mapsto_aux.(unseal).
   Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
@@ -123,9 +123,14 @@ Section definitions.
 End definitions.
 Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
-Local Notation "l ↦{ q } v" := (mapsto l q%dfrac v)
-  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
-Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v) (at level 20) : bi_scope.
+Declare Custom Entry dfrac.
+Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
+Notation "â–¡" := DfracDiscarded (in custom dfrac).
+Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
+Notation "" := (DfracOwn 1) (in custom dfrac).
+
+Local Notation "l ↦ dq v" := (mapsto l dq v)
+  (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
 
 Section gen_heap.
   Context {L V} `{Countable L, !gen_heapG L V Σ}.
@@ -137,7 +142,7 @@ Section gen_heap.
   Implicit Types v : V.
 
   (** General properties of mapsto *)
-  Global Instance mapsto_timeless l q v : Timeless (l ↦{q} v).
+  Global Instance mapsto_timeless l dq v : Timeless (l ↦{dq} v).
   Proof. rewrite mapsto_eq. apply _. Qed.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{#q} v)%I.
   Proof.
@@ -146,30 +151,30 @@ Section gen_heap.
   Global Instance mapsto_as_fractional l q v :
     AsFractional (l ↦{#q} v) (λ q, l ↦{#q} v)%I q.
   Proof. split; [done|]. apply _. Qed.
-  Global Instance mapsto_persistent l v : Persistent (l ↦{#□} v).
+  Global Instance mapsto_persistent l v : Persistent (l ↦□ v).
   Proof. rewrite mapsto_eq. apply _. Qed.
 
-  Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜✓ q⌝%Qp.
+  Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%Qp.
   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) ∧ v1 = v2⌝.
+  Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
   Proof.
     rewrite mapsto_eq. iIntros "H1 H2".
     iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
     auto.
   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⌝.
+  Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
     iIntros "H1 H2".
     iDestruct (mapsto_valid_2 with "H1 H2") as %[_ ?].
     done.
   Qed.
 
-  Lemma mapsto_combine l q1 q2 v1 v2 :
-    l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ l ↦{q1 ⋅ q2} v1 ∗ ⌜v1 = v2⌝.
+  Lemma mapsto_combine l dq1 dq2 v1 v2 :
+    l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
   Proof.
     iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
     iCombine "Hl1 Hl2" as "Hl".
@@ -177,18 +182,18 @@ Section gen_heap.
     auto.
   Qed.
 
-  Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
-    ¬ ✓(q1 ⋅ q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+  Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
+    ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof.
     iIntros (?) "Hl1 Hl2"; iIntros (->).
     by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
   Qed.
-  Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+  Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof. apply mapsto_frac_ne. intros ?%exclusive_l; [done|apply _]. Qed.
 
   (** Permanently turn a fractional points-to predicate into a persistent
       points-to predicate. *)
-  Lemma mapsto_persist l q v : l ↦{#q} v ==∗ l ↦{#□} v.
+  Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
   Proof. rewrite mapsto_eq. apply own_update, gmap_view_persist. Qed.
 
   (** General properties of [meta] and [meta_token] *)
@@ -280,7 +285,7 @@ Section gen_heap.
       first by apply lookup_union_None.
   Qed.
 
-  Lemma gen_heap_valid σ l q v : gen_heap_interp σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
+  Lemma gen_heap_valid σ l dq v : gen_heap_interp σ -∗ l ↦{dq} v -∗ ⌜σ !! l = Some v⌝.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
     rewrite /gen_heap_interp mapsto_eq.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 18f4a1fe1a8ea69641402447cc30f2c0472b1e45..c4fe31053359b4db23244fc79300a15ee617569a 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -14,12 +14,10 @@ From iris.prelude Require Import options.
 (** The [array] connective is a version of [mapsto] that works
 with lists of values. *)
 
-Definition array `{!heapG Σ} (l : loc) (q : dfrac) (vs : list val) : iProp Σ :=
-  ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{q} v)%I.
-Notation "l ↦∗{ q } vs" := (array l q%dfrac vs)
-  (at level 20, q at level 50, format "l  ↦∗{ q }  vs") : bi_scope.
-Notation "l ↦∗ vs" := (array l (DfracOwn 1) vs)
-  (at level 20, format "l  ↦∗  vs") : bi_scope.
+Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
+  ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v)%I.
+Notation "l ↦∗ dq vs" := (array l dq vs)
+  (at level 20, dq custom dfrac  at level 1, format "l  ↦∗ dq  vs") : bi_scope.
 
 (** We have [FromSep] and [IntoSep] instances to split the fraction (via the
 [AsFractional] instance below), but not for splitting the list, as that would
@@ -42,21 +40,21 @@ Global Instance array_as_fractional l q vs :
   AsFractional (l ↦∗{#q} vs) (λ q, l ↦∗{#q} vs)%I q.
 Proof. split; done || apply _. Qed.
 
-Lemma array_nil l q : l ↦∗{q} [] ⊣⊢ emp.
+Lemma array_nil l dq : l ↦∗{dq} [] ⊣⊢ emp.
 Proof. by rewrite /array. Qed.
 
-Lemma array_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
+Lemma array_singleton l dq v : l ↦∗{dq} [v] ⊣⊢ l ↦{dq} v.
 Proof. by rewrite /array /= right_id loc_add_0. Qed.
 
-Lemma array_app l q vs ws :
-  l ↦∗{q} (vs ++ ws) ⊣⊢ l ↦∗{q} vs ∗ (l +ₗ length vs) ↦∗{q} ws.
+Lemma array_app l dq vs ws :
+  l ↦∗{dq} (vs ++ ws) ⊣⊢ l ↦∗{dq} vs ∗ (l +ₗ length vs) ↦∗{dq} ws.
 Proof.
   rewrite /array big_sepL_app.
   setoid_rewrite Nat2Z.inj_add.
   by setoid_rewrite loc_add_assoc.
 Qed.
 
-Lemma array_cons l q v vs : l ↦∗{q} (v :: vs) ⊣⊢ l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vs.
+Lemma array_cons l dq v vs : l ↦∗{dq} (v :: vs) ⊣⊢ l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs.
 Proof.
   rewrite /array big_sepL_cons loc_add_0.
   setoid_rewrite loc_add_assoc.
@@ -64,14 +62,14 @@ Proof.
   by setoid_rewrite Z.add_1_l.
 Qed.
 
-Global Instance array_cons_frame l q v vs R Q :
-  Frame false R (l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vs) Q →
-  Frame false R (l ↦∗{q} (v :: vs)) Q.
+Global Instance array_cons_frame l dq v vs R Q :
+  Frame false R (l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs) Q →
+  Frame false R (l ↦∗{dq} (v :: vs)) Q.
 Proof. by rewrite /Frame array_cons. Qed.
 
-Lemma update_array l q vs off v :
+Lemma update_array l dq vs off v :
   vs !! off = Some v →
-  ⊢ l ↦∗{q} vs -∗ ((l +ₗ off) ↦{q} v ∗ ∀ v', (l +ₗ off) ↦{q} v' -∗ l ↦∗{q} <[off:=v']>vs).
+  ⊢ l ↦∗{dq} vs -∗ ((l +ₗ off) ↦{dq} v ∗ ∀ v', (l +ₗ off) ↦{dq} v' -∗ l ↦∗{dq} <[off:=v']>vs).
 Proof.
   iIntros (Hlookup) "Hl".
   rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
@@ -89,9 +87,9 @@ Proof.
 Qed.
 
 (** * Rules for allocation *)
-Lemma mapsto_seq_array l q v n :
-  ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦{q} v) -∗
-  l ↦∗{q} replicate n v.
+Lemma mapsto_seq_array l dq v n :
+  ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦{dq} v) -∗
+  l ↦∗{dq} replicate n v.
 Proof.
   rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
   { done. }
@@ -143,9 +141,9 @@ Proof.
 Qed.
 
 (** * Rules for accessing array elements *)
-Lemma twp_load_offset s E l q off vs v :
+Lemma twp_load_offset s E l dq off vs v :
   vs !! off = Some v →
-  [[{ l ↦∗{q} vs }]] ! #(l +ₗ off) @ s; E [[{ RET v; l ↦∗{q} vs }]].
+  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ off) @ s; E [[{ RET v; l ↦∗{dq} vs }]].
 Proof.
   iIntros (Hlookup Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
@@ -153,19 +151,19 @@ Proof.
   iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
   iApply "Hl2". iApply "Hl1".
 Qed.
-Lemma wp_load_offset s E l q off vs v :
+Lemma wp_load_offset s E l dq off vs v :
   vs !! off = Some v →
-  {{{ ▷ l ↦∗{q} vs }}} ! #(l +ₗ off) @ s; E {{{ RET v; l ↦∗{q} vs }}}.
+  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ off) @ s; E {{{ RET v; l ↦∗{dq} vs }}}.
 Proof.
   iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_load_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) :
-  [[{ l ↦∗{q} vs }]] ! #(l +ₗ off) @ s; E [[{ RET vs !!! off; l ↦∗{q} vs }]].
+Lemma twp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
+  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ off) @ s; E [[{ RET vs !!! off; l ↦∗{dq} vs }]].
 Proof. apply twp_load_offset. by apply vlookup_lookup. Qed.
-Lemma wp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) :
-  {{{ ▷ l ↦∗{q} vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗{q} vs }}}.
+Lemma wp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
+  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗{dq} vs }}}.
 Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
 
 Lemma twp_store_offset s E l off vs v :
@@ -244,13 +242,13 @@ Proof.
   iApply (twp_cmpxchg_suc_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_cmpxchg_fail_offset s E l q off vs v0 v1 v2 :
+Lemma twp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
   vs !! off = Some v0 →
   v0 ≠ v1 →
   vals_compare_safe v0 v1 →
-  [[{ l ↦∗{q} vs }]]
+  [[{ l ↦∗{dq} vs }]]
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  [[{ RET (v0, #false); l ↦∗{q} vs }]].
+  [[{ RET (v0, #false); l ↦∗{dq} vs }]].
 Proof.
   iIntros (Hlookup HNEq Hcmp Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
@@ -259,31 +257,31 @@ Proof.
   iIntros "Hl1". iApply "HΦ". iDestruct ("Hl2" $! v0) as "Hl2".
   rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".
 Qed.
-Lemma wp_cmpxchg_fail_offset s E l q off vs v0 v1 v2 :
+Lemma wp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
   vs !! off = Some v0 →
   v0 ≠ v1 →
   vals_compare_safe v0 v1 →
-  {{{ ▷ l ↦∗{q} vs }}}
+  {{{ ▷ l ↦∗{dq} vs }}}
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (v0, #false); l ↦∗{q} vs }}}.
+  {{{ RET (v0, #false); l ↦∗{dq} vs }}}.
 Proof.
   iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_cmpxchg_fail_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_cmpxchg_fail_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) v1 v2 :
+Lemma twp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v1 v2 :
   vs !!! off ≠ v1 →
   vals_compare_safe (vs !!! off) v1 →
-  [[{ l ↦∗{q} vs }]]
+  [[{ l ↦∗{dq} vs }]]
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  [[{ RET (vs !!! off, #false); l ↦∗{q} vs }]].
+  [[{ RET (vs !!! off, #false); l ↦∗{dq} vs }]].
 Proof. intros. eapply twp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
-Lemma wp_cmpxchg_fail_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) v1 v2 :
+Lemma wp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v1 v2 :
   vs !!! off ≠ v1 →
   vals_compare_safe (vs !!! off) v1 →
-  {{{ ▷ l ↦∗{q} vs }}}
+  {{{ ▷ l ↦∗{dq} vs }}}
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (vs !!! off, #false); l ↦∗{q} vs }}}.
+  {{{ RET (vs !!! off, #false); l ↦∗{dq} vs }}}.
 Proof. intros. eapply wp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
 
 Lemma twp_faa_offset s E l off vs (i1 i2 : Z) :
@@ -348,11 +346,11 @@ Proof.
   iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
 Qed.
 
-Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
+Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) dq v' v1 v2 v :
   v' ≠ v1 → vals_compare_safe v' v1 →
-  {{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
+  {{{ proph p pvs ∗ ▷ l ↦{dq} v' }}}
     Resolve (CmpXchg #l v1 v2) #p v @ s; E
-  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
+  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{dq} v' }}}.
 Proof.
   iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
   iApply (wp_resolve with "Hp"); first done.
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index e8d64a3c764b6e845446b2168844b3994dad1232..94a7fc428df86b00308bea70bc87b43f1f8831c9 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -70,11 +70,11 @@ Section proof.
     iApply (twp_array_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
   Qed.
 
-  Lemma twp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
+  Lemma twp_array_copy_to stk E (dst src : loc) vdst vsrc dq (n : Z) :
     Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
-    [[{ dst ↦∗ vdst ∗ src ↦∗{q} vsrc }]]
+    [[{ dst ↦∗ vdst ∗ src ↦∗{dq} vsrc }]]
       array_copy_to #dst #src #n @ stk; E
-    [[{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{q} vsrc }]].
+    [[{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{dq} vsrc }]].
   Proof.
     iIntros (Hvdst Hvsrc Φ) "[Hdst Hsrc] HΦ".
     iInduction vdst as [|v1 vdst] "IH" forall (n dst src vsrc Hvdst Hvsrc);
@@ -87,22 +87,22 @@ Section proof.
     iIntros "[Hvdst Hvsrc]".
     iApply "HΦ"; by iFrame.
   Qed.
-  Lemma wp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
+  Lemma wp_array_copy_to stk E (dst src : loc) vdst vsrc dq (n : Z) :
     Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
-    {{{ dst ↦∗ vdst ∗ src ↦∗{q} vsrc }}}
+    {{{ dst ↦∗ vdst ∗ src ↦∗{dq} vsrc }}}
       array_copy_to #dst #src #n @ stk; E
-    {{{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{q} vsrc }}}.
+    {{{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{dq} vsrc }}}.
   Proof.
     iIntros (? ? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
     iApply (twp_array_copy_to with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
   Qed.
 
-  Lemma twp_array_clone stk E l q vl n :
+  Lemma twp_array_clone stk E l dq vl n :
     Z.of_nat (length vl) = n →
     (0 < n)%Z →
-    [[{ l ↦∗{q} vl }]]
+    [[{ l ↦∗{dq} vl }]]
       array_clone #l #n @ stk; E
-    [[{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} vl }]].
+    [[{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{dq} vl }]].
   Proof.
     iIntros (Hvl Hn Φ) "Hvl HΦ".
     wp_lam.
@@ -114,12 +114,12 @@ Section proof.
       wp_pures.
       iApply "HΦ"; by iFrame.
   Qed.
-  Lemma wp_array_clone stk E l q vl n :
+  Lemma wp_array_clone stk E l dq vl n :
     Z.of_nat (length vl) = n →
     (0 < n)%Z →
-    {{{ l ↦∗{q} vl }}}
+    {{{ l ↦∗{dq} vl }}}
       array_clone #l #n @ stk; E
-    {{{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} vl }}}.
+    {{{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{dq} vl }}}.
   Proof.
     iIntros (? ? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
     iApply (twp_array_clone with "H"); [auto..|]; iIntros (l') "H HΦ". by iApply "HΦ".
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 08c8a4412910fb5b50aba3e1183222b596211ab3..f40d17bd74dd02e7be931ec47b4d036e7660c393 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -47,13 +47,8 @@ Arguments atomic_heap _ {_}.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
 Module notation.
-Notation "l ↦{ q } v" := (mapsto l q%dfrac v)
-  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
-Notation "l ↦ v" := (mapsto l (DfracOwn 1) v) (at level 20) : bi_scope.
-
-Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
-  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
-Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
+otation "l ↦ dq v" := (mapsto l dq v)
+  (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
 
 Notation "'ref' e" := (alloc e) : expr_scope.
 Notation "! e" := (load e) : expr_scope.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 7952803e879ad8cb931e17b55723a3c342fcb56e..4d3c577a92af795a7729b3d8c496cdad6d69ccd6 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -28,10 +28,10 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
 
 (** Since we use an [option val] instance of [gen_heap], we need to overwrite
 the notations.  That also helps for scopes and coercions. *)
-Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=option val) l q%dfrac (Some v%V))
-  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
 Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
   (at level 20) : bi_scope.
+Notation "l ↦ dq v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
+  (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
 
 (** Same for [gen_inv_heap], except that these are higher-order notations so to
 make setoid rewriting in the predicate [I] work we need actual definitions
@@ -277,30 +277,30 @@ Qed.
 (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
 value type being [option val]. *)
 
-Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜✓ q⌝%Qp.
+Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%Qp.
 Proof. apply mapsto_valid. Qed.
-Lemma mapsto_valid_2 l q1 q2 v1 v2 :
-  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 ⋅ q2) ∧ v1 = v2⌝.
+Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
+  l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ 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⌝.
+Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
 Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
 
-Lemma mapsto_combine l q1 q2 v1 v2 :
-  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ l ↦{q1 ⋅ q2} v1 ∗ ⌜v1 = v2⌝.
+Lemma mapsto_combine l dq1 dq2 v1 v2 :
+  l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
 Proof.
   iIntros "Hl1 Hl2". iDestruct (mapsto_combine with "Hl1 Hl2") as "[$ Heq]".
   by iDestruct "Heq" as %[= ->].
 Qed.
 
-Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
-  ¬ ✓(q1 ⋅ q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
+  ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_frac_ne. Qed.
-Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_ne. Qed.
 
-Lemma mapsto_persist l q v : l ↦{#q} v ==∗ l ↦{#□} v.
+Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
 Proof. apply mapsto_persist. Qed.
 
 Global Instance inv_mapsto_own_proper l v :
@@ -449,16 +449,16 @@ Proof.
   iApply (twp_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_load s E l q v :
-  [[{ l ↦{q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{q} v }]].
+Lemma twp_load s E l dq v :
+  [[{ l ↦{dq} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{dq} v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
-Lemma wp_load s E l q v :
-  {{{ ▷ l ↦{q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{q} v }}}.
+Lemma wp_load s E l dq v :
+  {{{ ▷ l ↦{dq} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{dq} v }}}.
 Proof.
   iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_load with "H"). iIntros "H HΦ". by iApply "HΦ".
@@ -482,10 +482,10 @@ Proof.
   iApply (twp_store with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
-Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
+Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
   v' ≠ v1 → vals_compare_safe v' v1 →
-  [[{ l ↦{q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }]].
+  [[{ l ↦{dq} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  [[{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -493,10 +493,10 @@ Proof.
   rewrite bool_decide_false //.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
-Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
+Lemma wp_cmpxchg_fail s E l dq v' v1 v2 :
   v' ≠ v1 → vals_compare_safe v' v1 →
-  {{{ ▷ l ↦{q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }}}.
+  {{{ ▷ l ↦{dq} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  {{{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' }}}.
 Proof.
   iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_cmpxchg_fail with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 57f3cc49e6ec9a58dfe135b2b782894a0a289605..d0657618951424e9104d6153de9aaf238170c39c 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -74,8 +74,8 @@
   heapG0 : heapG Σ
   l : loc
   ============================
-  "Hl1" : l ↦{#(1 / 2)} #0
-  "Hl2" : l ↦{#(1 / 2)} #0
+  "Hl1" : l ↦{#1 / 2} #0
+  "Hl2" : l ↦{#1 / 2} #0
   --------------------------------------∗
   |={⊤}=> True
   
@@ -124,10 +124,10 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   l : loc
   vs : list val
   ============================
-  "Hl1" : l ↦∗{#(1 / 2)} vs
-  "Hl2" : l ↦∗{#(1 / 2)} vs
+  "Hl1" : l ↦∗{#1 / 2} vs
+  "Hl2" : l ↦∗{#1 / 2} vs
   --------------------------------------∗
-  l ↦∗{#(1 / 2)} vs ∗ l ↦∗{#(1 / 2)} vs
+  l ↦∗{#1 / 2} vs ∗ l ↦∗{#1 / 2} vs
   
 "test_wp_finish_fupd"
      : string
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index eea231e956cd444a16ddd3eb838e460e87c76ea2..2d43b14bf78ae95e70d1ef6daa327c6261c77384 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -212,14 +212,14 @@ Section tests.
 
   Check "test_array_fraction_destruct".
   Lemma test_array_fraction_destruct l vs :
-    l ↦∗ vs -∗ l ↦∗{#(1/2)} vs ∗ l ↦∗{#(1/2)} vs.
+    l ↦∗ vs -∗ l ↦∗{#1/2} vs ∗ l ↦∗{#1/2} vs.
   Proof.
     iIntros "[Hl1 Hl2]". Show.
     by iFrame.
   Qed.
 
   Lemma test_array_fraction_combine l vs :
-    l ↦∗{#(1/2)} vs -∗ l↦∗{#(1/2)} vs -∗ l ↦∗ vs.
+    l ↦∗{#1/2} vs -∗ l↦∗{#1/2} vs -∗ l ↦∗ vs.
   Proof.
     iIntros "Hl1 Hl2".
     iSplitL "Hl1"; by iFrame.
@@ -233,7 +233,7 @@ Section tests.
   Qed.
 
   Lemma test_array_app_split l vs1 vs2 :
-    l ↦∗ (vs1 ++ vs2) -∗ l ↦∗{#(1/2)} (vs1 ++ vs2).
+    l ↦∗ (vs1 ++ vs2) -∗ l ↦∗{#1/2} (vs1 ++ vs2).
   Proof.
     iIntros "[$ _]". (* splits the fraction, not the app *)
   Qed.
@@ -270,24 +270,24 @@ Section persistent_mapsto_tests.
 
   (* Loading from a persistent points-to predicate in the _persistent_ context. *)
   Lemma persistent_mapsto_load_persistent l v :
-    {{{ l ↦{#□} v }}} ! #l {{{ RET v; True }}}.
+    {{{ l ↦□ v }}} ! #l {{{ RET v; True }}}.
   Proof. iIntros (Φ) "#Hl HΦ". wp_load. by iApply "HΦ". Qed.
 
   (* Loading from a persistent points-to predicate in the _spatial_ context. *)
   Lemma persistent_mapsto_load_spatial l v :
-    {{{ l ↦{#□} v }}} ! #l {{{ RET v; True }}}.
+    {{{ l ↦□ v }}} ! #l {{{ RET v; True }}}.
   Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.
 
   Lemma persistent_mapsto_twp_load_persistent l v :
-    [[{ l ↦{#□} v }]] ! #l [[{ RET v; True }]].
+    [[{ l ↦□ v }]] ! #l [[{ RET v; True }]].
   Proof. iIntros (Φ) "#Hl HΦ". wp_load. by iApply "HΦ". Qed.
 
   Lemma persistent_mapsto_twp_load_spatial l v :
-    [[{ l ↦{#□} v }]] ! #l [[{ RET v; True }]].
+    [[{ l ↦□ v }]] ! #l [[{ RET v; True }]].
   Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.
 
   Lemma persistent_mapsto_load l (n : nat) :
-    {{{ l ↦ #n }}} Store #l (! #l + #5) ;; ! #l {{{ RET #(n + 5); l ↦{#□} #(n + 5) }}}.
+    {{{ l ↦ #n }}} Store #l (! #l + #5) ;; ! #l {{{ RET #(n + 5); l ↦□ #(n + 5) }}}.
   Proof.
     iIntros (Φ) "Hl HΦ".
     wp_load. wp_store.