diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index 24bac65b35decd0e526a12210893d72168f607c8..f18259973cd016644e30815b7d5a907439201fdb 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -389,12 +389,21 @@ Section cmra.
     intros Hup. rewrite -(right_id _ _ (●V a')).
     apply view_update=> n bf. rewrite left_id. apply Hup.
   Qed.
+
   Lemma view_update_auth a a' b' :
-    (∀ n bf, rel n a bf → rel n a' bf) → ●V a ~~> ●V a'.
+    (∀ n bf, rel n a bf → rel n a' bf) →
+    ●V a ~~> ●V a'.
   Proof.
     intros Hup. rewrite -(right_id _ _ (●V a)) -(right_id _ _ (●V a')).
     apply view_update=> n bf. rewrite !left_id. apply Hup.
   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.
+  Qed.
 
   Lemma view_update_alloc_frac q a b :
     (∀ n bf, rel n a bf → rel n a (b ⋅ bf)) →