diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1d11d393074660c6864f4e013ad6b97bb81b1b56..59ed387aef40f42bfd6c9dc39b562a41d8badd8a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -49,6 +49,8 @@ With this release, we dropped support for Coq 8.9.
 * Move the `*_validI` and `*_equivI` lemmas to a new module, `base_logic.algebra`.
   That module is exported by `base_logic.base_logic` so it should usually be
   available everywhere without further changes.
+* The authoritative fragment `✓ (◯ b : auth A)` is no longer definitionally
+  equal to `✓ b`.
 
 **Changes in `proofmode`:**
 
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 241c20e444e3f97ff656c3992dea10aec966fdae..3ad8bad9381797a748194af0f5b6cf25851506a2 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -28,11 +28,21 @@ Qed.
 Lemma auth_view_rel_raw_valid (A : ucmraT) n (a b : A) :
   auth_view_rel_raw n a b → ✓{n} b.
 Proof. intros [??]; eauto using cmra_validN_includedN. Qed.
+Lemma auth_view_rel_raw_unit (A : ucmraT) n :
+  ∃ a : A, auth_view_rel_raw n a ε.
+Proof. exists ε. split; [done|]. apply ucmra_unit_validN. Qed.
 Canonical Structure auth_view_rel {A : ucmraT} : view_rel A A :=
-  ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A) (auth_view_rel_raw_valid A).
+  ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A)
+          (auth_view_rel_raw_valid A) (auth_view_rel_raw_unit A).
 
 Lemma auth_view_rel_unit {A : ucmraT} n (a : A) : auth_view_rel n a ε ↔ ✓{n} a.
 Proof. split; [by intros [??]|]. split; auto using ucmra_unit_leastN. Qed.
+Lemma auth_view_rel_exists {A : ucmraT} n (b : A) :
+  (∃ a, auth_view_rel n a b) ↔ ✓{n} b.
+Proof.
+  split; [|intros; exists b; by split].
+  intros [a Hrel]. eapply auth_view_rel_raw_valid, Hrel.
+Qed.
 
 Instance auth_view_rel_discrete {A : ucmraT} :
   CmraDiscrete A → ViewRelDiscrete (auth_view_rel (A:=A)).
@@ -94,8 +104,17 @@ Section auth.
   Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
   Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
-  Lemma auth_frag_validN n a : ✓{n} (◯ a) ↔ ✓{n} a.
-  Proof. apply view_frag_validN. Qed.
+  Lemma auth_frag_validN n b : ✓{n} (◯ b) ↔ ✓{n} b.
+  Proof. by rewrite view_frag_validN auth_view_rel_exists. Qed.
+  (** Also stated as implications, which can be used to force [apply] to use the
+  lemma in the right direction. *)
+  Lemma auth_frag_op_validN n b1 b2 : ✓{n} (◯ b1 ⋅ ◯ b2) ↔ ✓{n} (b1 ⋅ b2).
+  Proof. apply auth_frag_validN. Qed.
+  Lemma auth_frag_op_validN_1 n b1 b2 : ✓{n} (◯ b1 ⋅ ◯ b2) → ✓{n} (b1 ⋅ b2).
+  Proof. apply auth_frag_op_validN. Qed.
+  Lemma auth_frag_op_validN_2 n b1 b2 : ✓{n} (b1 ⋅ b2) → ✓{n} (◯ b1 ⋅ ◯ b2).
+  Proof. apply auth_frag_op_validN. Qed.
+
   Lemma auth_both_frac_validN n q a b :
     ✓{n} (●{q} a ⋅ ◯ b) ↔ ✓{n} q ∧ b ≼{n} a ∧ ✓{n} a.
   Proof. apply view_both_frac_validN. Qed.
@@ -112,8 +131,19 @@ Section auth.
     rewrite view_auth_valid !cmra_valid_validN.
     by setoid_rewrite auth_view_rel_unit.
   Qed.
-  Lemma auth_frag_valid a : ✓ (◯ a) ↔ ✓ a.
-  Proof. apply view_frag_valid. Qed.
+  Lemma auth_frag_valid b : ✓ (◯ b) ↔ ✓ b.
+  Proof.
+    rewrite view_frag_valid cmra_valid_validN.
+    by setoid_rewrite auth_view_rel_exists.
+  Qed.
+  (** Also stated as implications, which can be used to force [apply] to use the
+  lemma in the right direction. *)
+  Lemma auth_frag_op_valid b1 b2 : ✓ (◯ b1 ⋅ ◯ b2) ↔ ✓ (b1 ⋅ b2).
+  Proof. apply auth_frag_valid. Qed.
+  Lemma auth_frag_op_valid_1 b1 b2 : ✓ (◯ b1 ⋅ ◯ b2) → ✓ (b1 ⋅ b2).
+  Proof. apply auth_frag_op_valid. Qed.
+  Lemma auth_frag_op_valid_2 b1 b2 : ✓ (b1 ⋅ b2) → ✓ (◯ b1 ⋅ ◯ b2).
+  Proof. apply auth_frag_op_valid. Qed.
 
   (** These lemma statements are a bit awkward as we cannot possibly extract a
   single witness for [b ≼ a] from validity, we have to make do with one witness
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index d317c918f4f84cc18754e89460a1aa2d44e28930..8624b79a53e2e49e3ae6d2dac35143c13d5faeb6 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -84,9 +84,9 @@ Section frac_auth.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.
 
   Lemma frac_auth_frag_validN n q a : ✓{n} (◯F{q} a) ↔ ✓{n} q ∧ ✓{n} a.
-  Proof. done. Qed.
+  Proof. by rewrite /frac_auth_frag auth_frag_validN. Qed.
   Lemma frac_auth_frag_valid q a : ✓ (◯F{q} a) ↔ ✓ q ∧ ✓ a.
-  Proof. done. Qed.
+  Proof. by rewrite /frac_auth_frag auth_frag_valid. Qed.
 
   Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2.
   Proof. done. Qed.
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index f9e9ebe010aba57cb8fd23699ad2a05c3a3f0146..58971fb413439ce06064893dd0e1e16e057b2d01 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -27,7 +27,8 @@ Local Definition gmap_view_fragUR (K : Type) `{Countable K} (V : ofeT) : ucmraT
 (** View relation. *)
 Section rel.
   Context (K : Type) `{Countable K} (V : ofeT).
-  Implicit Types (m : gmap K V) (k : K) (v : V) (n : nat) (f : gmap_view_fragUR K V).
+  Implicit Types (m : gmap K V) (k : K) (v : V) (n : nat).
+  Implicit Types (f : gmap K (dfrac * agree V)).
 
   Local Definition gmap_view_rel_raw n m f : Prop :=
     map_Forall (λ k dv, ∃ v, dv.2 ≡{n}≡ to_agree v ∧ ✓ dv.1 ∧ m !! k = Some v) f.
@@ -75,8 +76,37 @@ Section rel.
     - rewrite Hagree. done.
   Qed.
 
+  Local Lemma gmap_view_rel_raw_unit n :
+    ∃ m, gmap_view_rel_raw n m ε.
+  Proof. exists ∅. apply: map_Forall_empty. Qed.
+
   Local Canonical Structure gmap_view_rel : view_rel (gmapO K V) (gmap_view_fragUR K V) :=
-    ViewRel gmap_view_rel_raw gmap_view_rel_raw_mono gmap_view_rel_raw_valid.
+    ViewRel gmap_view_rel_raw gmap_view_rel_raw_mono
+            gmap_view_rel_raw_valid gmap_view_rel_raw_unit.
+
+  Local Lemma gmap_view_rel_exists n (f : gmap K (dfrac * agreeR V)) :
+    (∃ m, gmap_view_rel n m f) ↔ ✓{n} f.
+  Proof.
+    split.
+    { intros [m Hrel]. eapply gmap_view_rel_raw_valid, Hrel. }
+    intros Hf.
+    cut (∃ m, gmap_view_rel n m f ∧ ∀ k, f !! k = None → m !! k = None).
+    { naive_solver. }
+    induction f as [|k [dq ag] f Hk' IH] using map_ind.
+    { exists ∅. split; [|done]. apply: map_Forall_empty. }
+    move: (Hf k). rewrite lookup_insert=> -[/= ??].
+    destruct (to_agree_uninjN n ag) as [v ?]; [done|].
+    destruct IH as (m & Hm & Hdom).
+    { intros k'. destruct (decide (k = k')) as [->|?]; [by rewrite Hk'|].
+      move: (Hf k'). by rewrite lookup_insert_ne. }
+    exists (<[k:=v]> m).
+    rewrite /gmap_view_rel /= /gmap_view_rel_raw map_Forall_insert //=. split_and!.
+    - exists v. by rewrite lookup_insert.
+    - eapply map_Forall_impl; [apply Hm|]; simpl.
+      intros k' [dq' ag'] (v'&?&?&?). exists v'.
+      rewrite lookup_insert_ne; naive_solver.
+    - intros k'. rewrite !lookup_insert_None. naive_solver.
+  Qed.
 
   Local Lemma gmap_view_rel_discrete :
     OfeDiscrete V → ViewRelDiscrete gmap_view_rel.
@@ -148,15 +178,13 @@ Section lemmas.
 
   Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
   Proof.
-    rewrite view_frag_validN singleton_validN. split.
-    - intros [??]. done.
-    - intros ?. split; done.
+    rewrite view_frag_validN gmap_view_rel_exists singleton_validN pair_validN.
+    naive_solver.
   Qed.
   Lemma gmap_view_frag_valid k dq v : ✓ gmap_view_frag k dq v ↔ ✓ dq.
   Proof.
-    rewrite view_frag_valid singleton_valid. split.
-    - intros [??]. done.
-    - intros ?. split; done.
+    rewrite cmra_valid_validN. setoid_rewrite gmap_view_frag_validN.
+    naive_solver eauto using O.
   Qed.
 
   Lemma gmap_view_frag_op k dq1 dq2 v :
@@ -171,18 +199,15 @@ Section lemmas.
     ✓{n} (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔
       ✓ (dq1 ⋅ dq2) ∧ v1 ≡{n}≡ v2.
   Proof.
-    rewrite view_frag_validN singleton_op singleton_validN -pair_op.
-    split; intros [Hfrac Hagree]; (split; first done); simpl in *.
-    - apply to_agree_op_invN. done.
-    - rewrite Hagree agree_idemp. done.
+    rewrite view_frag_validN gmap_view_rel_exists singleton_op singleton_validN.
+    by rewrite -pair_op pair_validN to_agree_op_validN.
   Qed.
   Lemma gmap_view_frag_op_valid k dq1 dq2 v1 v2 :
     ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
   Proof.
-    rewrite view_frag_valid singleton_op singleton_valid -pair_op.
-    split; intros [Hfrac Hagree]; (split; first done); simpl in *.
-    - apply to_agree_op_inv. done.
-    - rewrite Hagree agree_idemp. done.
+    rewrite view_frag_valid. setoid_rewrite gmap_view_rel_exists.
+    rewrite -cmra_valid_validN singleton_op singleton_valid.
+    by rewrite -pair_op pair_valid to_agree_op_valid.
   Qed.
   Lemma gmap_view_frag_op_valid_L `{!LeibnizEquiv V} k dq1 dq2 v1 v2 :
     ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 = v2.
@@ -278,10 +303,7 @@ Section lemmas.
   Lemma gmap_view_persist k q v :
     gmap_view_frag k (DfracOwn q) v ~~> gmap_view_frag k DfracDiscarded v.
   Proof.
-    apply view_update_frag; last first.
-    { eapply singleton_update, prod_update; simpl; last done.
-      apply dfrac_discard_update. }
-    move=>m n bf Hrel j [df va] /=.
+    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).
@@ -314,7 +336,6 @@ Section lemmas.
     IsOp dq dq1 dq2 →
     IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v) (gmap_view_frag k dq2 v).
   Proof. rewrite /IsOp' /IsOp => ->. apply gmap_view_frag_op. Qed.
-
 End lemmas.
 
 (** Functor *)
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index 791eeab78c5c4116f4ed908d5467ed3695f19baa..89954f77ee2ab964bc7619582c150eb13daacf68 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -49,7 +49,9 @@ Structure view_rel (A : ofeT) (B : ucmraT) := ViewRel {
     n2 ≤ n1 →
     view_rel_holds n2 a2 b2;
   view_rel_validN n a b :
-    view_rel_holds n a b → ✓{n} b
+    view_rel_holds n a b → ✓{n} b;
+  view_rel_unit n :
+    ∃ a, view_rel_holds n a ε
 }.
 Arguments ViewRel {_ _} _ _.
 Arguments view_rel_holds {_ _} _ _ _ _.
@@ -175,13 +177,13 @@ Section cmra.
     match view_auth_proj x with
     | Some (q, ag) =>
        ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
-    | None => ✓ view_frag_proj x
+    | None => ∀ n, ∃ a, rel n a (view_frag_proj x)
     end.
   Instance view_validN : ValidN (view rel) := λ n x,
     match view_auth_proj x with
     | Some (q, ag) =>
        ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
-    | None => ✓{n} view_frag_proj x
+    | None => ∃ a, rel n a (view_frag_proj x)
     end.
   Instance view_pcore : PCore (view rel) := λ x,
     Some (View (core (view_auth_proj x)) (core (view_frag_proj x))).
@@ -193,13 +195,13 @@ Section cmra.
       match view_auth_proj x with
       | Some (q, ag) =>
          ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
-      | None => ✓ view_frag_proj x
+      | None => ∀ n, ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
   Local Definition view_validN_eq :
     validN = λ n x, 
       match view_auth_proj x with
       | Some (q, ag) => ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
-      | None => ✓{n} view_frag_proj x
+      | None => ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
 
   Lemma view_auth_frac_validN n q a : ✓{n} (●V{q} a) ↔ ✓{n} q ∧ rel n a ε.
@@ -211,7 +213,7 @@ Section cmra.
   Proof.
     rewrite view_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
   Qed.
-  Lemma view_frag_validN n b : ✓{n} (◯V b) ↔ ✓{n} b.
+  Lemma view_frag_validN n b : ✓{n} (◯V b) ↔ ∃ a, rel n a b.
   Proof. done. Qed.
   Lemma view_both_frac_validN n q a b :
     ✓{n} (●V{q} a ⋅ ◯V b) ↔ ✓{n} q ∧ rel n a b.
@@ -232,7 +234,7 @@ Section cmra.
   Qed.
   Lemma view_auth_valid a : ✓ (●V a) ↔ ∀ n, rel n a ε.
   Proof. rewrite view_auth_frac_valid frac_valid'. naive_solver. Qed.
-  Lemma view_frag_valid b : ✓ (◯V b) ↔ ✓ b.
+  Lemma view_frag_valid b : ✓ (◯V b) ↔ ∀ n, ∃ a, rel n a b.
   Proof. done. Qed.
   Lemma view_both_frac_valid q a b : ✓ (●V{q} a ⋅ ◯V b) ↔ ✓ q ∧ ∀ n, rel n a b.
   Proof.
@@ -249,16 +251,19 @@ Section cmra.
       (λ x : option (frac * agree A) * B, View x.1 x.2)
       (λ x, (view_auth_proj x, view_frag_proj x))); try done.
     - intros [x b]. by rewrite /= pair_pcore !cmra_pcore_core.
-    - intros n [[[q ag]|] b]; rewrite /= view_validN_eq /=; last done.
-      intros (?&a&->&?). repeat split; simpl; [done|]. by eapply view_rel_validN.
+    - intros n [[[q ag]|] b]; rewrite /= view_validN_eq /=.
+      + intros (?&a&->&?). repeat split; simpl; [done|]. by eapply view_rel_validN.
+      + intros [a ?]. repeat split; simpl. by eapply view_rel_validN.
     - rewrite view_validN_eq.
       intros n [x1 b1] [x2 b2] [Hx ?]; simpl in *;
         destruct Hx as [[q1 ag1] [q2 ag2] [??]|]; intros ?; by ofe_subst.
     - rewrite view_valid_eq view_validN_eq.
-      intros [[[q aa]|] b]; rewrite /= cmra_valid_validN; naive_solver.
-    - rewrite view_validN_eq=> n [[[q ag]|] b] /=; [|by eauto using cmra_validN_S].
-      intros [? (a&?&?)]; split; [done|]. exists a; split; [by eauto using dist_S|].
-      apply view_rel_mono with (S n) a b; auto with lia.
+      intros [[[q aa]|] b]; rewrite /= ?cmra_valid_validN; naive_solver.
+    - rewrite view_validN_eq=> n [[[q ag]|] b] /=.
+      + intros [? (a&?&?)]; split; [done|].
+        exists a; split; [by eauto using dist_S|].
+        apply view_rel_mono with (S n) a b; auto with lia.
+      + intros [a ?]. exists a. apply view_rel_mono with (S n) a b; auto with lia.
     - rewrite view_validN_eq=> n [[[q1 ag1]|] b1] [[[q2 ag2]|] b2] /=.
       + intros [?%cmra_validN_op_l (a & Haga & ?)]. split; [done|].
         assert (ag1 ≡{n}≡ ag2) as Ha12 by (apply agree_op_invN; by rewrite Haga).
@@ -266,8 +271,10 @@ Section cmra.
         apply view_rel_mono with n a (b1 â‹… b2); eauto using cmra_includedN_l.
       + intros [? (a & Haga & ?)]. split; [done|]. exists a; split; [done|].
         apply view_rel_mono with n a (b1 â‹… b2); eauto using cmra_includedN_l.
-      + intros [? (a & Haga & ?%view_rel_validN)]. eauto using cmra_validN_op_l.
-      + eauto using cmra_validN_op_l.
+      + intros [? (a & Haga & ?)]. exists a.
+        apply view_rel_mono with n a (b1 â‹… b2); eauto using cmra_includedN_l.
+      + intros [a ?]. exists a.
+        apply view_rel_mono with n a (b1 â‹… b2); eauto using cmra_includedN_l.
   Qed.
   Canonical Structure viewR := CmraT (view rel) view_cmra_mixin.
 
@@ -284,14 +291,14 @@ Section cmra.
     split; [apply _|]=> -[[[q ag]|] b]; rewrite view_valid_eq view_validN_eq /=.
     - rewrite -cmra_discrete_valid_iff.
       setoid_rewrite <-(discrete_iff _ ag). naive_solver.
-    - by rewrite -cmra_discrete_valid_iff.
+    - naive_solver.
   Qed.
 
   Instance view_empty : Unit (view rel) := View ε ε.
   Lemma view_ucmra_mixin : UcmraMixin (view rel).
   Proof.
     split; simpl.
-    - rewrite view_valid_eq /=. apply ucmra_unit_valid.
+    - rewrite view_valid_eq /=. apply view_rel_unit.
     - by intros x; constructor; rewrite /= left_id.
     - do 2 constructor; [done| apply (core_id_core _)].
   Qed.
@@ -461,10 +468,9 @@ Section cmra.
   Qed.
   Lemma view_update_frag b b' :
     (∀ a n bf, rel n a (b ⋅ bf) → rel n a (b' ⋅ bf)) →
-    b ~~> b' →
     â—¯V b ~~> â—¯V b'.
   Proof.
-    rewrite !cmra_total_update view_validN_eq=> ?? n [[[q ag]|] bf]; naive_solver.
+    rewrite !cmra_total_update view_validN_eq=> ? n [[[q ag]|] bf]; naive_solver.
   Qed.
 
   Lemma view_update_frac_alloc q a b :
diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index d185f4a17e814a11003842cec8fa7569ce1a2510..149ff33bccc680ead53f6e6c99137b01f57fd6d9 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -187,8 +187,10 @@ Section view.
     ✓ (●V a : view rel) ⊣⊢ relI.
   Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
 
-  Lemma view_frag_validI b : ✓ (◯V b : view rel) ⊣⊢@{uPredI M} ✓ b.
-  Proof. by uPred.unseal. Qed.
+  Lemma view_frag_validI (relI : uPred M) b :
+    (∀ n (x : M), relI n x ↔ ∃ a, rel n a b) →
+    ✓ (◯V b : view rel) ⊣⊢@{uPredI M} relI.
+  Proof. uPred.unseal=> Hrel. split=> n x _. by rewrite Hrel. Qed.
 End view.
 
 Section auth.
@@ -207,7 +209,10 @@ Section auth.
   Qed.
 
   Lemma auth_frag_validI a : ✓ (◯ a) ⊣⊢@{uPredI M} ✓ a.
-  Proof. apply view_frag_validI. Qed.
+  Proof.
+    apply view_frag_validI=> n x.
+    rewrite auth_view_rel_exists. by uPred.unseal.
+  Qed.
 
   Lemma auth_both_frac_validI q a b :
     ✓ (●{q} a ⋅ ◯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
@@ -245,13 +250,12 @@ Section gmap_view.
   Qed.
 
   Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
-    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊢@{uPredI M}
-      ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
+    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢@{uPredI M}
+    ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
   Proof.
-    rewrite /gmap_view_frag -view_frag_op view_frag_validI.
-    rewrite singleton_op singleton_validI -pair_op prod_validI /=.
-    apply bi.and_mono; first done.
-    rewrite agree_validI agree_equivI. done.
+    rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n x.
+    rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
+    rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
   Qed.
 End gmap_view.
 
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 0f3f693e97cbf067baec6eec55bbc29017a8df0d..850db347dbc634cdf2b8fce87b8bc69d1d2bb16b 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -5,7 +5,6 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Export lock.
 From iris Require Import options.
-Import uPred.
 
 Definition wait_loop: val :=
   rec: "wait_loop" "x" "lk" :=
@@ -67,7 +66,7 @@ Section proof.
   Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof.
     iDestruct 1 as (o1) "H1". iDestruct 1 as (o2) "H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[[] _].
+    iDestruct (own_valid_2 with "H1 H2") as %[[] _]%auth_frag_op_valid_1.
   Qed.
 
   Lemma is_lock_iff γ lk R1 R2 :
@@ -105,7 +104,8 @@ Section proof.
         { iNext. iExists o, n. iFrame. }
         wp_pures. case_bool_decide; [|done]. wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
-      + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
+      + iDestruct (own_valid_2 with "Ht Haown")
+          as %[_ ?%gset_disj_valid_op]%auth_frag_op_valid_1.
         set_solver.
     - iModIntro. iSplitL "Hlo Hln Ha".
       { iNext. iExists o, n. by iFrame. }
@@ -160,7 +160,7 @@ Section proof.
     iDestruct (own_valid_2 with "Hauth Hγo") as
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
     iDestruct "Haown" as "[[Hγo' _]|Haown]".
-    { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
+    { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]%auth_frag_op_valid_1. }
     iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
     { apply auth_update, prod_local_update_1.
       by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 29a4e0e03b898001f4337f8ac6c27981c2ece661..2a0fde9be9cfb4750221ddb65cf8fa66356e59e4 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -94,7 +94,9 @@ Section lifting.
       as %[->%Excl_included _]%auth_both_valid_discrete.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
-  Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
+  Proof.
+    rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_valid_op_1_l).
+  Qed.
   Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.