diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5413e760ec0dcde2da508038d671da3f663b2700..84728002c18915e6dd316a88557882ef5507f393 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -73,11 +73,12 @@ Chajed, and Yusuke Matsushita. Thanks a lot to everyone involved!
 
 **Changes in `algebra`:**
 
-* Generalize the authorative elements of the `view`, `auth` and `gset_bij`
-  cameras to be parameterized by a [discardable fraction](iris/algebra/dfrac.v)
-  (`dfrac`) instead of a fraction (`frac`). Normal fractions are now denoted
-  `●{#q} a` and `●V{#q} a`. Lemmas affected by this have been renamed such that
-  the "frac" in their name has been changed into "dfrac". (by Simon Friis Vindum)
+* Generalize the authorative elements of the `view`, `auth`, `gmap_view`, and
+  `gset_bij` cameras to be parameterized by a [discardable
+  fraction](iris/algebra/dfrac.v) (`dfrac`) instead of a fraction (`frac`).
+  Normal fractions are now denoted `●{#q} a` and `●V{#q} a`. Lemmas affected by
+  this have been renamed such that the "frac" in their name has been changed
+  into "dfrac". (by Simon Friis Vindum)
 * Generalize `namespace_map` to `reservation_map` which enhances `gmap positive
   A` with a notion of 'tokens' that enable allocating a particular name in the
   map. See [algebra.reservation_map](iris/algebra/reservation_map.v) for further
@@ -218,11 +219,13 @@ replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
 Note that the script is not idempotent, do not run it twice.
 ```
 sed -i -E -f- $(find theories -name "*.v") <<EOF
-# auth and view renames from frac to dfrac
+# auth, view, and gmap_view renames from frac to dfrac
 s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_validN|valid|op_valid|valid_2|valid_discrete|includedN|included|alloc|validI|validI_2|validI_1|validI|)\b/\1_\2_dfrac_\3/g
 s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
 s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
 s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
+s/\bgmap_view_(auth|both)_frac_(op_invN|op_inv|op_inv_L|valid|op_validN|op_valid|op_valid_L)\b/gmap_view_\1_dfrac_\2/g
+s/\bgmap_view_persist\b/gmap_view_frag_persist/g
 # big_sepM renames
 s/\bbig_sepM2_lookup_1\b/big_sepM2_lookup_l/g
 s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 9ea02bf6360393f6bb1eca97eecd023b8c395635..aa19988e144d0d79306ac1cda20e5f8c426649cd 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -137,8 +137,8 @@ Definition gmap_viewUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
 Section definitions.
   Context {K : Type} `{Countable K} {V : ofe}.
 
-  Definition gmap_view_auth (q : frac) (m : gmap K V) : gmap_viewR K V :=
-    ●V{#q} m.
+  Definition gmap_view_auth (dq : dfrac) (m : gmap K V) : gmap_viewR K V :=
+    ●V{dq} m.
   Definition gmap_view_frag (k : K) (dq : dfrac) (v : V) : gmap_viewR K V :=
     â—¯V {[k := (dq, to_agree v)]}.
 End definitions.
@@ -148,9 +148,9 @@ Section lemmas.
   Implicit Types (m : gmap K V) (k : K) (q : Qp) (dq : dfrac) (v : V).
 
   Global Instance : Params (@gmap_view_auth) 5 := {}.
-  Global Instance gmap_view_auth_ne q : NonExpansive (gmap_view_auth (K:=K) (V:=V) q).
+  Global Instance gmap_view_auth_ne dq : NonExpansive (gmap_view_auth (K:=K) (V:=V) dq).
   Proof. solve_proper. Qed.
-  Global Instance gmap_view_auth_proper q : Proper ((≡) ==> (≡)) (gmap_view_auth (K:=K) (V:=V) q).
+  Global Instance gmap_view_auth_proper dq : Proper ((≡) ==> (≡)) (gmap_view_auth (K:=K) (V:=V) dq).
   Proof. apply ne_proper, _. Qed.
 
   Global Instance : Params (@gmap_view_frag) 6 := {}.
@@ -176,49 +176,54 @@ Section lemmas.
   Qed.
 
   (** Composition and validity *)
+  Lemma gmap_view_auth_dfrac_op dp dq m :
+    gmap_view_auth (dp ⋅ dq) m ≡
+    gmap_view_auth dp m â‹… gmap_view_auth dq m.
+  Proof. by rewrite /gmap_view_auth view_auth_dfrac_op. Qed.
   Lemma gmap_view_auth_frac_op p q m :
-    gmap_view_auth (p + q) m ≡ gmap_view_auth p m ⋅ gmap_view_auth q m.
-  Proof. by rewrite /gmap_view_auth -dfrac_op_own view_auth_dfrac_op. Qed.
-  Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
-    IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
+    gmap_view_auth (DfracOwn (p + q)) m ≡
+    gmap_view_auth (DfracOwn p) m â‹… gmap_view_auth (DfracOwn q) m.
+  Proof. by rewrite /gmap_view_auth view_auth_frac_op. Qed.
+  Global Instance gmap_view_auth_dfrac_is_op dq dq1 dq2 m :
+    IsOp dq dq1 dq2 → IsOp' (gmap_view_auth dq m) (gmap_view_auth dq1 m) (gmap_view_auth dq2 m).
   Proof. rewrite /gmap_view_auth. apply _. Qed.
 
-  Lemma gmap_view_auth_frac_op_invN n p m1 q m2 :
-    ✓{n} (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡{n}≡ m2.
+  Lemma gmap_view_auth_dfrac_op_invN n dp m1 dq m2 :
+    ✓{n} (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 ≡{n}≡ m2.
   Proof. apply view_auth_dfrac_op_invN. Qed.
-  Lemma gmap_view_auth_frac_op_inv p m1 q m2 :
-    ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡ m2.
+  Lemma gmap_view_auth_dfrac_op_inv dp m1 dq m2 :
+    ✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 ≡ m2.
   Proof. apply view_auth_dfrac_op_inv. Qed.
-  Lemma gmap_view_auth_frac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
-    ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 = m2.
+  Lemma gmap_view_auth_dfrac_op_inv_L `{!LeibnizEquiv V} dq m1 dp m2 :
+    ✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 = m2.
   Proof. apply view_auth_dfrac_op_inv_L, _. Qed.
 
-  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ (q ≤ 1)%Qp.
+  Lemma gmap_view_auth_dfrac_valid m dq : ✓ gmap_view_auth dq m ↔ ✓ dq.
   Proof.
     rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
-  Lemma gmap_view_auth_valid m : ✓ gmap_view_auth 1 m.
-  Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
+  Lemma gmap_view_auth_valid m : ✓ gmap_view_auth (DfracOwn 1) m.
+  Proof. rewrite gmap_view_auth_dfrac_valid. done. Qed.
 
-  Lemma gmap_view_auth_frac_op_validN n q1 q2 m1 m2 :
-    ✓{n} (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 ≡{n}≡ m2.
+  Lemma gmap_view_auth_dfrac_op_validN n dq1 dq2 m1 m2 :
+    ✓{n} (gmap_view_auth dq1 m1 ⋅ gmap_view_auth dq2 m2) ↔ ✓ (dq1 ⋅ dq2) ∧ m1 ≡{n}≡ m2.
   Proof.
     rewrite view_auth_dfrac_op_validN. intuition eauto using gmap_view_rel_unit.
   Qed.
-  Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
-    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ (q1 + q2 ≤ 1)%Qp ∧ m1 ≡ m2.
+  Lemma gmap_view_auth_dfrac_op_valid dq1 dq2 m1 m2 :
+    ✓ (gmap_view_auth dq1 m1 ⋅ gmap_view_auth dq2 m2) ↔ ✓ (dq1 ⋅ dq2) ∧ m1 ≡ m2.
   Proof.
     rewrite view_auth_dfrac_op_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
-  Lemma gmap_view_auth_frac_op_valid_L `{!LeibnizEquiv V} q1 q2 m1 m2 :
-    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 = m2.
-  Proof. unfold_leibniz. apply gmap_view_auth_frac_op_valid. Qed.
+  Lemma gmap_view_auth_dfrac_op_valid_L `{!LeibnizEquiv V} dq1 dq2 m1 m2 :
+    ✓ (gmap_view_auth dq1 m1 ⋅ gmap_view_auth dq2 m2) ↔ ✓ (dq1 ⋅ dq2) ∧ m1 = m2.
+  Proof. unfold_leibniz. apply gmap_view_auth_dfrac_op_valid. Qed.
 
   Lemma gmap_view_auth_op_validN n m1 m2 :
-    ✓{n} (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
+    ✓{n} (gmap_view_auth (DfracOwn 1) m1 ⋅ gmap_view_auth (DfracOwn 1) m2) ↔ False.
   Proof. apply view_auth_op_validN. Qed.
   Lemma gmap_view_auth_op_valid m1 m2 :
-    ✓ (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
+    ✓ (gmap_view_auth (DfracOwn 1) m1 ⋅ gmap_view_auth (DfracOwn 1) m2) ↔ False.
   Proof. apply view_auth_op_valid. Qed.
 
   Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
@@ -260,21 +265,21 @@ Section lemmas.
     ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 = v2.
   Proof. unfold_leibniz. apply gmap_view_frag_op_valid. Qed.
 
-  Lemma gmap_view_both_frac_validN n q m k dq v :
-    ✓{n} (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-      (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
+  Lemma gmap_view_both_dfrac_validN n dp m k dq v :
+    ✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
+      ✓ dp ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
     rewrite view_both_dfrac_validN gmap_view_rel_lookup.
     naive_solver.
   Qed.
   Lemma gmap_view_both_validN n m k dq v :
-    ✓{n} (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
+    ✓{n} (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ↔
       ✓ dq ∧ m !! k ≡{n}≡ Some v.
-  Proof. rewrite gmap_view_both_frac_validN. naive_solver done. Qed.
-  Lemma gmap_view_both_frac_valid q m k dq v :
-    ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-    (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡ Some v.
+  Proof. rewrite gmap_view_both_dfrac_validN. naive_solver done. Qed.
+  Lemma gmap_view_both_dfrac_valid dp m k dq v :
+    ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
+    ✓ dp ∧ ✓ dq ∧ m !! k ≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
     rewrite view_both_dfrac_valid. setoid_rewrite gmap_view_rel_lookup.
@@ -286,18 +291,18 @@ Section lemmas.
       + apply Hm.
       + revert n. apply equiv_dist. apply Hm.
   Qed.
-  Lemma gmap_view_both_frac_valid_L `{!LeibnizEquiv V} q m k dq v :
-    ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-    ✓ q ∧ ✓ dq ∧ m !! k = Some v.
-  Proof. unfold_leibniz. apply gmap_view_both_frac_valid. Qed.
+  Lemma gmap_view_both_dfrac_valid_L `{!LeibnizEquiv V} dp m k dq v :
+    ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
+    ✓ dp ∧ ✓ dq ∧ m !! k = Some v.
+  Proof. unfold_leibniz. apply gmap_view_both_dfrac_valid. Qed.
   Lemma gmap_view_both_valid m k dq v :
-    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
+    ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ↔
     ✓ dq ∧ m !! k ≡ Some v.
-  Proof. rewrite gmap_view_both_frac_valid. naive_solver done. Qed.
+  Proof. rewrite gmap_view_both_dfrac_valid. naive_solver done. Qed.
   (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
      have [inv_L] lemmas instead that just have an equality on the RHS. *)
   Lemma gmap_view_both_valid_L `{!LeibnizEquiv V} m k dq v :
-    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
+    ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ↔
     ✓ dq ∧ m !! k = Some v.
   Proof. unfold_leibniz. apply gmap_view_both_valid. Qed.
 
@@ -305,7 +310,7 @@ Section lemmas.
   Lemma gmap_view_alloc m k dq v :
     m !! k = None →
     ✓ dq →
-    gmap_view_auth 1 m ~~> gmap_view_auth 1 (<[k := v]> m) â‹… gmap_view_frag k dq v.
+    gmap_view_auth (DfracOwn 1) m ~~> gmap_view_auth (DfracOwn 1) (<[k := v]> m) â‹… gmap_view_frag k dq v.
   Proof.
     intros Hfresh Hdq. apply view_update_alloc=>n bf Hrel j [df va] /=.
     rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
@@ -326,8 +331,8 @@ Section lemmas.
   Lemma gmap_view_alloc_big m m' dq :
     m' ##ₘ m →
     ✓ dq →
-    gmap_view_auth 1 m ~~>
-      gmap_view_auth 1 (m' ∪ m) ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
+    gmap_view_auth (DfracOwn 1) m ~~>
+      gmap_view_auth (DfracOwn 1) (m' ∪ m) ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
   Proof.
     intros. induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
     { rewrite big_opM_empty left_id_L right_id. done. }
@@ -339,8 +344,8 @@ Section lemmas.
   Qed.
 
   Lemma gmap_view_delete m k v :
-    gmap_view_auth 1 m â‹… gmap_view_frag k (DfracOwn 1) v ~~>
-    gmap_view_auth 1 (delete k m).
+    gmap_view_auth (DfracOwn 1) m â‹… gmap_view_frag k (DfracOwn 1) v ~~>
+    gmap_view_auth (DfracOwn 1) (delete k m).
   Proof.
     apply view_update_dealloc=>n bf Hrel j [df va] Hbf /=.
     destruct (decide (j = k)) as [->|Hne].
@@ -354,8 +359,8 @@ Section lemmas.
   Qed.
 
   Lemma gmap_view_delete_big m m' :
-    gmap_view_auth 1 m ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k (DfracOwn 1) v) ~~>
-    gmap_view_auth 1 (m ∖ m').
+    gmap_view_auth (DfracOwn 1) m ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k (DfracOwn 1) v) ~~>
+    gmap_view_auth (DfracOwn 1) (m ∖ m').
   Proof.
     induction m' as [|k v m' ? IH] using map_ind.
     { rewrite right_id_L big_opM_empty right_id //. }
@@ -365,8 +370,8 @@ Section lemmas.
   Qed.
 
   Lemma gmap_view_update m k v v' :
-    gmap_view_auth 1 m â‹… gmap_view_frag k (DfracOwn 1) v ~~>
-      gmap_view_auth 1 (<[k := v']> m) â‹… gmap_view_frag k (DfracOwn 1) v'.
+    gmap_view_auth (DfracOwn 1) m â‹… gmap_view_frag k (DfracOwn 1) v ~~>
+      gmap_view_auth (DfracOwn 1) (<[k := v']> m) â‹… gmap_view_frag k (DfracOwn 1) v'.
   Proof.
     rewrite gmap_view_delete.
     rewrite (gmap_view_alloc _ k (DfracOwn 1) v') //; last by rewrite lookup_delete.
@@ -375,8 +380,8 @@ Section lemmas.
 
   Lemma gmap_view_update_big m m0 m1 :
     dom (gset K) m0 = dom (gset K) m1 →
-    gmap_view_auth 1 m ⋅ ([^op map] k↦v ∈ m0, gmap_view_frag k (DfracOwn 1) v) ~~>
-      gmap_view_auth 1 (m1 ∪ m) ⋅ ([^op map] k↦v ∈ m1, gmap_view_frag k (DfracOwn 1) v).
+    gmap_view_auth (DfracOwn 1) m ⋅ ([^op map] k↦v ∈ m0, gmap_view_frag k (DfracOwn 1) v) ~~>
+      gmap_view_auth (DfracOwn 1) (m1 ∪ m) ⋅ ([^op map] k↦v ∈ m1, gmap_view_frag k (DfracOwn 1) v).
   Proof.
     intros Hdom%eq_sym. revert m1 Hdom.
     induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom.
@@ -398,7 +403,11 @@ Section lemmas.
     rewrite union_delete_insert //.
   Qed.
 
-  Lemma gmap_view_persist k dq v :
+  Lemma gmap_view_auth_persist dq m :
+    gmap_view_auth dq m ~~> gmap_view_auth DfracDiscarded m.
+  Proof. apply view_update_auth_persist. Qed.
+
+  Lemma gmap_view_frag_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] /=.
diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 138969cfca5b87a2767ffbb2149a2e74a0a630c0..2cfccb368e306d0e8c526218d11044ecf0c7e9e0 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -244,7 +244,7 @@ Section gmap_view.
   Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
 
   Lemma gmap_view_both_validI m k dq v :
-    ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ⊢
+    ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ⊢
     ✓ dq ∧ m !! k ≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index d8a8d713f30a81c37ae9a94b0a9b21f5f3c52dff..e59bb24129b138f54c798d1f8a69709b5f3b8587 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -25,7 +25,7 @@ Section definitions.
   Context `{ghost_mapG Σ K V}.
 
   Definition ghost_map_auth_def (γ : gname) (q : Qp) (m : gmap K V) : iProp Σ :=
-    own γ (gmap_view_auth (V:=leibnizO V) q m).
+    own γ (gmap_view_auth (V:=leibnizO V) (DfracOwn q) m).
   Definition ghost_map_auth_aux : seal (@ghost_map_auth_def). Proof. by eexists. Qed.
   Definition ghost_map_auth := ghost_map_auth_aux.(unseal).
   Definition ghost_map_auth_eq : @ghost_map_auth = @ghost_map_auth_def := ghost_map_auth_aux.(seal_eq).
@@ -117,7 +117,7 @@ Section lemmas.
   (** Make an element read-only. *)
   Lemma ghost_map_elem_persist k γ dq v :
     k ↪[γ]{dq} v ==∗ k ↪[γ]□ v.
-  Proof. unseal. iApply own_update. apply gmap_view_persist. Qed.
+  Proof. unseal. iApply own_update. apply gmap_view_frag_persist. Qed.
 
   (** * Lemmas about [ghost_map_auth] *)
   Lemma ghost_map_alloc_strong P m :
@@ -125,7 +125,7 @@ Section lemmas.
     ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ ghost_map_auth γ 1 m ∗ [∗ map] k ↦ v ∈ m, k ↪[γ] v.
   Proof.
     unseal. intros.
-    iMod (own_alloc_strong (gmap_view_auth (V:=leibnizO V) 1 ∅) P)
+    iMod (own_alloc_strong (gmap_view_auth (V:=leibnizO V) (DfracOwn 1) ∅) P)
       as (γ) "[% Hauth]"; first done.
     { apply gmap_view_auth_valid. }
     iExists γ. iSplitR; first done.
@@ -165,14 +165,14 @@ Section lemmas.
   Lemma ghost_map_auth_valid γ q m : ghost_map_auth γ q m -∗ ⌜q ≤ 1⌝%Qp.
   Proof.
     unseal. iIntros "Hauth".
-    iDestruct (own_valid with "Hauth") as %?%gmap_view_auth_frac_valid.
+    iDestruct (own_valid with "Hauth") as %?%gmap_view_auth_dfrac_valid.
     done.
   Qed.
   Lemma ghost_map_auth_valid_2 γ q1 q2 m1 m2 :
     ghost_map_auth γ q1 m1 -∗ ghost_map_auth γ q2 m2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ m1 = m2⌝.
   Proof.
     unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_auth_frac_op_valid_L.
+    iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_auth_dfrac_op_valid_L.
     done.
   Qed.
   Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :
@@ -188,7 +188,7 @@ Section lemmas.
     ghost_map_auth γ q m -∗ k ↪[γ]{dq} v -∗ ⌜m !! k = Some v⌝.
   Proof.
     unseal. iIntros "Hauth Hel".
-    iDestruct (own_valid_2 with "Hauth Hel") as %[?[??]]%gmap_view_both_frac_valid_L.
+    iDestruct (own_valid_2 with "Hauth Hel") as %[?[??]]%gmap_view_both_dfrac_valid_L.
     eauto.
   Qed.
 
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 1b3b210d772a941fc1c84877938aae411aa01f55..8667560e652691d2e76afe4f3dbd80e738930bc3 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -51,7 +51,7 @@ Global Instance: Params (@ownD) 3 := {}.
 
 Definition wsat `{!invGS Σ} : iProp Σ :=
   locked (∃ I : gmap positive (iProp Σ),
-    own invariant_name (gmap_view_auth 1 (invariant_unfold <$> I)) ∗
+    own invariant_name (gmap_view_auth (DfracOwn 1) (invariant_unfold <$> I)) ∗
     [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
 
 Section wsat.
@@ -103,7 +103,7 @@ Lemma ownD_singleton_twice i : ownD {[i]} ∗ ownD {[i]} ⊢ False.
 Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.
 
 Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
-  own invariant_name (gmap_view_auth 1 (invariant_unfold <$> I)) ∗
+  own invariant_name (gmap_view_auth (DfracOwn 1) (invariant_unfold <$> I)) ∗
   own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)) ⊢
   ∃ Q, ⌜I !! i = Some Q⌝ ∗ ▷ (Q ≡ P).
 Proof.
@@ -185,7 +185,7 @@ End wsat.
 Lemma wsat_alloc `{!invGpreS Σ} : ⊢ |==> ∃ _ : invGS Σ, wsat ∗ ownE ⊤.
 Proof.
   iIntros.
-  iMod (own_alloc (gmap_view_auth 1 ∅)) as (γI) "HI";
+  iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γI) "HI";
     first by apply gmap_view_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.