diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 3a38ffa34c1de63c409f3b2c1055f2865e745abf..f0cd0c5bce2db23c5615ce6be3db152c52443d2f 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -271,7 +271,7 @@ Qed.
 
 Instance: ∀ x : agree A, NonExpansive (op x).
 Proof.
-  intros x n y1 y2. rewrite /dist /agree_dist /agree_list /=. 
+  intros x n y1 y2. rewrite /dist /agree_dist /agree_list /=.
   rewrite !app_comm_cons. apply: list_setequiv_app.
 Qed.
 Instance: NonExpansive2 (@op (agree A) _).
@@ -353,7 +353,7 @@ Qed.
 Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
 
 Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
-Proof. intros a b [Hxy%list_setincl_singleton_rev _]. done. Qed. 
+Proof. intros a b [Hxy%list_setincl_singleton_rev _]. done. Qed.
 Global Instance to_agree_inj : Inj (≡) (≡) (to_agree).
 Proof.
   intros a b ?. apply equiv_dist=>n. apply to_agree_injN. by apply equiv_dist.
@@ -387,14 +387,35 @@ Proof.
   - intros Hab. rewrite Hab. eexists. symmetry. eapply agree_idemp.
 Qed.
 
-Lemma to_agree_comp_valid (a b : A) : ✓ (to_agree a ⋅ to_agree b) ↔ a ≡ b.
+Lemma to_agree_comp_validN n (a b : A) :
+  ✓{n} (to_agree a ⋅ to_agree b) ↔ a ≡{n}≡ b.
 Proof.
   split.
-  - (* TODO: can this be derived from other stuff?  Otherwise, should probably become sth. generic about list_agrees. *)
+  - (* TODO: can this be derived from other stuff?  Otherwise, should probably
+       become sth. generic about list_agrees. *)
     intros Hv. apply Hv; simpl; set_solver.
   - intros ->. rewrite agree_idemp. done.
 Qed.
 
+Lemma to_agree_comp_valid (a b : A) : ✓ (to_agree a ⋅ to_agree b) ↔ a ≡ b.
+Proof.
+  rewrite cmra_valid_validN equiv_dist. by setoid_rewrite to_agree_comp_validN.
+Qed.
+
+Global Instance agree_cancelable (x : agree A) : Cancelable x.
+Proof.
+  intros n y z Hv Heq.
+  destruct (to_agree_uninjN n x) as [x' EQx]; first by eapply cmra_validN_op_l.
+  destruct (to_agree_uninjN n y) as [y' EQy]; first by eapply cmra_validN_op_r.
+  destruct (to_agree_uninjN n z) as [z' EQz].
+  { eapply (cmra_validN_op_r n x z). by rewrite -Heq. }
+  assert (Hx'y' : x' ≡{n}≡ y').
+  { apply to_agree_comp_validN. by rewrite EQx EQy. }
+  assert (Hx'z' : x' ≡{n}≡ z').
+  { apply to_agree_comp_validN. by rewrite EQx EQz -Heq. }
+  by rewrite -EQy -EQz -Hx'y' -Hx'z'.
+Qed.
+
 (** Internalized properties *)
 Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M).
 Proof.
@@ -425,7 +446,7 @@ Section agree_map.
   Proof using Hyps.
     intros n x y Hxy.
     change (list_setequiv (dist n)(f <$> (agree_list x))(f <$> (agree_list y))).
-    eapply list_setequiv_fmap; last exact Hxy. apply _. 
+    eapply list_setequiv_fmap; last exact Hxy. apply _.
   Qed.
   Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _.
 
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3f1c99a1055baa5c832166f5d1d34ba4e064bbdd..c60bfe6c2828dc2703e50f3e2538a458bab71b8e 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -137,6 +137,18 @@ Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → Fal
 Arguments exclusive0_l {_} _ {_} _ _.
 Hint Mode Exclusive + ! : typeclass_instances.
 
+(** * Cancelable elements. *)
+Class Cancelable {A : cmraT} (x : A) :=
+  cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
+Arguments cancelableN {_} _ {_} _ _ _ _.
+Hint Mode Cancelable + ! : typeclass_instances.
+
+(** * Identity-free elements. *)
+Class IdFree {A : cmraT} (x : A) :=
+  id_free0_r y : ✓{0}x → x ⋅ y ≡{0}≡ x → False.
+Arguments id_free0_r {_} _ {_} _ _.
+Hint Mode IdFree + ! : typeclass_instances.
+
 (** * CMRAs whose core is total *)
 (** The function [core] may return a dummy when used on CMRAs without total
 core. *)
@@ -310,11 +322,11 @@ Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
 Lemma cmra_pcore_l' x cx : pcore x ≡ Some cx → cx ⋅ x ≡ x.
 Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_l. Qed.
 Lemma cmra_pcore_r x cx : pcore x = Some cx → x ⋅ cx ≡ x.
-Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed. 
+Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed.
 Lemma cmra_pcore_r' x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed. 
+Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed.
 Lemma cmra_pcore_idemp' x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed. 
+Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed.
 Lemma cmra_pcore_dup x cx : pcore x = Some cx → cx ≡ cx ⋅ cx.
 Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
 Lemma cmra_pcore_dup' x cx : pcore x ≡ Some cx → cx ≡ cx ⋅ cx.
@@ -526,6 +538,60 @@ Proof.
   split; first by apply cmra_included_includedN.
   intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
 Qed.
+
+(** Cancelable elements  *)
+Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
+Proof. unfold Cancelable. intros ?? EQ. by setoid_rewrite EQ. Qed.
+Lemma cancelable x `{!Cancelable x} y z :
+  ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z.
+Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
+Lemma discrete_cancelable x `{CMRADiscrete A}:
+  (∀ y z, ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z) → Cancelable x.
+Proof. intros ????. rewrite -!timeless_iff -cmra_discrete_valid_iff. auto. Qed.
+Global Instance cancelable_op x y :
+  Cancelable x → Cancelable y → Cancelable (x ⋅ y).
+Proof.
+  intros ???????. apply (cancelableN y), (cancelableN x).
+  - eapply cmra_validN_op_r. by rewrite assoc.
+  - by rewrite assoc.
+  - by rewrite !assoc.
+Qed.
+Global Instance exclusive_cancelable (x : A) : Exclusive x → Cancelable x.
+Proof. intros ???? []%(exclusiveN_l _ x). Qed.
+
+(** Id-free elements  *)
+Global Instance id_free_ne : Proper (dist n ==> iff) (@IdFree A).
+Proof.
+  unfold IdFree. intros ??? EQ%(dist_le _ 0); last lia.
+  split; intros ??; (rewrite -EQ || rewrite EQ); eauto.
+Qed.
+Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A).
+Proof.
+  unfold IdFree. intros ?? EQ.
+  split; intros ??; (rewrite -EQ || rewrite EQ); eauto.
+Qed.
+Lemma id_freeN_r n n' x `{!IdFree x} y : ✓{n}x → x ⋅ y ≡{n'}≡ x → False.
+Proof. eauto using cmra_validN_le, dist_le with lia. Qed.
+Lemma id_freeN_l n n' x `{!IdFree x} y : ✓{n}x → y ⋅ x ≡{n'}≡ x → False.
+Proof. rewrite comm. eauto using id_freeN_r. Qed.
+Lemma id_free_r x `{!IdFree x} y : ✓x → x ⋅ y ≡ x → False.
+Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
+Lemma id_free_l x `{!IdFree x} y : ✓x → y ⋅ x ≡ x → False.
+Proof. rewrite comm. eauto using id_free_r. Qed.
+Lemma discrete_id_free x `{CMRADiscrete A}:
+  (∀ y, ✓x → x ⋅ y ≡ x → False) → IdFree x.
+Proof. repeat intro. eauto using cmra_discrete_valid, cmra_discrete, timeless. Qed.
+Global Instance id_free_op_r x y :
+  IdFree y → Cancelable x → IdFree (x ⋅ y).
+Proof.
+  intros ???? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
+  eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto].
+Qed.
+Global Instance id_free_op_l x y :
+  IdFree x → Cancelable y → IdFree (x ⋅ y).
+Proof. intros. rewrite comm. apply _. Qed.
+Global Instance exclusive_id_free x : Exclusive x → IdFree x.
+Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
 End cmra.
 
 (** * Properties about CMRAs with a unit element **)
@@ -549,6 +615,8 @@ Section ucmra.
     intros x. destruct (cmra_pcore_mono' ∅ x ∅) as (cx&->&?);
       eauto using ucmra_unit_least, (persistent (∅:A)).
   Qed.
+  Global Instance empty_cancelable : Cancelable (∅:A).
+  Proof. intros ???. by rewrite !left_id. Qed.
 End ucmra.
 Hint Immediate cmra_unit_total.
 
@@ -650,7 +718,7 @@ Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) :
   CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ∘ f).
 Proof.
   split.
-  - apply _. 
+  - apply _.
   - move=> n x Hx /=. by apply cmra_monotone_validN, cmra_monotone_validN.
   - move=> x y Hxy /=. by apply cmra_monotone, cmra_monotone.
 Qed.
@@ -674,7 +742,7 @@ Instance cmra_homomorphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
   CMRAHomomorphism f → CMRAHomomorphism g → CMRAHomomorphism (g ∘ f).
 Proof.
   split.
-  - apply _. 
+  - apply _.
   - move=> x y /=. rewrite -(cmra_homomorphism g).
     by apply (ne_proper _), cmra_homomorphism.
 Qed.
@@ -700,7 +768,7 @@ Structure rFunctor := RFunctor {
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
   rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
-    CMRAMonotone (rFunctor_map fg) 
+    CMRAMonotone (rFunctor_map fg)
 }.
 Existing Instances rFunctor_ne rFunctor_mono.
 Instance: Params (@rFunctor_map) 5.
@@ -868,6 +936,8 @@ Section unit.
   Proof. done. Qed.
   Global Instance unit_persistent (x : ()) : Persistent x.
   Proof. by constructor. Qed.
+  Global Instance unit_cancelable (x : ()) : Cancelable x.
+  Proof. by constructor. Qed.
 End unit.
 
 (** ** Natural numbers *)
@@ -901,6 +971,9 @@ Section nat.
 
   Global Instance nat_cmra_discrete : CMRADiscrete natR.
   Proof. constructor; apply _ || done. Qed.
+
+  Global Instance nat_cancelable (x : nat) : Cancelable x.
+  Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
 End nat.
 
 Definition mnat := nat.
@@ -964,6 +1037,13 @@ Section positive.
 
   Global Instance pos_cmra_discrete : CMRADiscrete positiveR.
   Proof. constructor; apply _ || done. Qed.
+  Global Instance pos_cancelable (x : positive) : Cancelable x.
+  Proof. intros ?????. by eapply Pos.add_reg_l, leibniz_equiv. Qed.
+  Global Instance pos_id_free (x : positive) : IdFree x.
+  Proof.
+    intros ???. edestruct Pos.add_no_neutral. rewrite Pos.add_comm.
+    by apply leibniz_equiv.
+  Qed.
 End positive.
 
 (** ** Product *)
@@ -1055,6 +1135,15 @@ Section prod.
   Proof. by intros ?[][?%exclusive0_l]. Qed.
   Global Instance pair_exclusive_r x y : Exclusive y → Exclusive (x,y).
   Proof. by intros ?[][??%exclusive0_l]. Qed.
+
+  Global Instance pair_cancelable x y :
+    Cancelable x → Cancelable y → Cancelable (x,y).
+  Proof. intros ???[][][][]. constructor; simpl in *; by eapply cancelableN. Qed.
+
+  Global Instance pair_id_free_l x y : IdFree x → IdFree (x,y).
+  Proof. move=>? [??] [? _] [/=? _]. eauto. Qed.
+  Global Instance pair_id_free_r x y : IdFree y → IdFree (x,y).
+  Proof. move=>? [??] [_ ?] [_ /=?]. eauto. Qed.
 End prod.
 
 Arguments prodR : clear implicits.
@@ -1259,6 +1348,20 @@ Section option.
 
   Lemma is_Some_included mx my : mx ≼ my → is_Some mx → is_Some my.
   Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
+
+  Global Instance cancelable_Some x :
+    IdFree x → Cancelable x → Cancelable (Some x).
+  Proof.
+    intros Hirr ?? [y|] [z|] ? EQ; inversion_clear EQ.
+    - constructor. by apply (cancelableN x).
+    - edestruct Hirr.
+      + eapply (cmra_validN_op_l 0 x y), (cmra_validN_le n). done. lia.
+      + eapply dist_le. done. lia.
+    - edestruct Hirr.
+      + eapply (cmra_validN_le n). done. lia.
+      + eapply dist_le. done. lia.
+    - done.
+  Qed.
 End option.
 
 Arguments optionR : clear implicits.
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 4fb69bd328e32a15c7f1b880cc146c4cb1d99248..fde21171bca57b53d3cee173d0fcdc6ed76f59af 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -181,9 +181,21 @@ Lemma csum_included x y :
                       ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼ b').
 Proof.
   split.
-  - intros [z Hy]; destruct x as [a|b|], z as [a'|b'|]; inversion_clear Hy; auto.
-    + right; left; eexists _, _; split_and!; eauto. eexists; eauto.
-    + right; right; eexists _, _; split_and!; eauto. eexists; eauto.
+  - unfold included. intros [[a'|b'|] Hy]; destruct x as [a|b|];
+      inversion_clear Hy; eauto 10.
+  - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
+    + destruct x; exists CsumBot; constructor.
+    + exists (Cinl c); by constructor.
+    + exists (Cinr c); by constructor.
+Qed.
+
+Lemma csum_includedN n x y :
+  x ≼{n} y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼{n} a')
+                         ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼{n} b').
+Proof.
+  split.
+  - unfold includedN. intros [[a'|b'|] Hy]; destruct x as [a|b|];
+      inversion_clear Hy; eauto 10.
   - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
     + destruct x; exists CsumBot; constructor.
     + exists (Cinl c); by constructor.
@@ -254,6 +266,22 @@ Proof. by move=> H[]? =>[/H||]. Qed.
 Global Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b).
 Proof. by move=> H[]? =>[|/H|]. Qed.
 
+Global Instance Cinl_cancelable a : Cancelable a → Cancelable (Cinl a).
+Proof.
+  move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ.
+  constructor. by eapply (cancelableN a).
+Qed.
+Global Instance Cinr_cancelable b : Cancelable b → Cancelable (Cinr b).
+Proof.
+  move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ.
+  constructor. by eapply (cancelableN b).
+Qed.
+
+Global Instance Cinl_id_free a : IdFree a → IdFree (Cinl a).
+Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
+Global Instance Cinr_id_free b : IdFree b → IdFree (Cinr b).
+Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
+
 Global Instance Cinl_cmra_homomorphism : CMRAHomomorphism Cinl.
 Proof. split. apply _. done. Qed.
 Global Instance Cinr_cmra_homomorphism : CMRAHomomorphism Cinr.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 6ba732e05c632e146b6ba82015b636f3831424bb..d00e7d9c4e75b0487e5abc9036b444d680fe5875 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -31,11 +31,19 @@ Qed.
 Canonical Structure fracR := discreteR frac frac_ra_mixin.
 End frac.
 
-(** Exclusive *)
 Global Instance frac_full_exclusive : Exclusive 1%Qp.
 Proof.
   move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
 Qed.
 
+Global Instance frac_cancelable (q : frac) : Cancelable q.
+Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
+
+Global Instance frac_id_free (q : frac) : IdFree q.
+Proof.
+  intros [q0 Hq0] ? EQ%Qp_eq. rewrite -{1}(Qcplus_0_r q) in EQ.
+  eapply Qclt_not_eq; first done. by apply (inj (Qcplus q)).
+Qed.
+
 Lemma frac_op': ∀ (p q: Qp), (p ⋅ q) = (p + q)%Qp.
 Proof. done. Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index bf43c466609794f2b6fe1f73809aa27f3cb51c23..36bd80ee99439aa7ac3c3caa5818d87ed4e6ceb6 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -156,7 +156,7 @@ Proof.
       + intros _. by rewrite lookup_op !lookup_delete Hi.
       + by rewrite !lookup_op lookup_insert_ne // !lookup_delete_ne. }
     destruct (cmra_extend n (Some x) (m1 !! i) (m2 !! i)) as (y1&y2&?&?&?).
-    { move: Hmv=> /(_ i). by rewrite lookup_insert. } 
+    { move: Hmv=> /(_ i). by rewrite lookup_insert. }
     { move: Hm=> /(_ i). by rewrite lookup_insert lookup_op. }
     exists (partial_alter (λ _, y1) i m1'), (partial_alter (λ _, y2) i m2').
     split_and!.
@@ -288,6 +288,17 @@ Proof.
     + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
 Qed.
 
+Global Instance singleton_cancelable i x :
+  Cancelable (Some x) → Cancelable {[ i := x ]}.
+Proof.
+  intros ???? Hv EQ j. specialize (EQ j). specialize (Hv j).
+  rewrite !lookup_op in EQ, Hv. destruct (decide (i = j)).
+  - subst. rewrite lookup_singleton in EQ, Hv.
+    by eapply cancelableN.
+  - rewrite lookup_singleton_ne // in EQ, Hv.
+    by rewrite ->!(left_id None _) in EQ.
+Qed.
+
 Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
   x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
 Proof.
@@ -435,7 +446,7 @@ Proof.
   - rewrite lookup_op !lookup_delete left_id symmetry_iff dist_None.
     apply eq_None_not_Some=> -[y Hi'].
     move: (Hmv i). rewrite Hm lookup_op Hi Hi' -Some_op. by apply exclusiveN_l.
-  - by rewrite lookup_op !lookup_delete_ne // lookup_op. 
+  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
 Qed.
 
 Lemma delete_singleton_local_update m i x `{!Exclusive x} :
@@ -444,6 +455,29 @@ Proof.
   rewrite -(delete_singleton i x).
   eapply delete_local_update; eauto using lookup_singleton.
 Qed.
+
+Lemma delete_local_update_cancelable m1 m2 i mx `{!Cancelable mx} :
+  m1 !! i ≡ mx → m2 !! i ≡ mx →
+  (m1, m2) ~l~> (delete i m1, delete i m2).
+Proof.
+  intros EQ1 EQ2.
+  destruct mx as [x|], (m1 !! i) as [m1i|] eqn:?, (m2 !! i) as [m2i|] eqn:?;
+    inversion_clear EQ1; inversion_clear EQ2.
+  - rewrite -{1}(insert_id m1 i m1i) // -{1}(insert_id m2 i m2i) //
+            -(insert_delete m1) -(insert_delete m2) !insert_singleton_op;
+    try by apply lookup_delete.
+    assert (m1i ≡ x) as -> by done. assert (m2i ≡ x) as -> by done.
+    apply cancel_local_update, _.
+  - rewrite !delete_notin //.
+Qed.
+
+Lemma delete_singleton_local_update_cancelable m i x `{!Cancelable (Some x)} :
+  m !! i ≡ Some x → (m, {[ i := x ]}) ~l~> (delete i m, ∅).
+Proof.
+  intros. rewrite -(delete_singleton i x).
+  apply (delete_local_update_cancelable m _ i (Some x));
+    [done|by rewrite lookup_singleton].
+Qed.
 End properties.
 
 (** Functor *)
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index e465e9e686344697260b51c6586483448e95ffd1..1c96c435d13f644f52c14543ead3ccde04d7461d 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -45,6 +45,13 @@ Section updates.
     by rewrite cmra_opM_assoc.
   Qed.
 
+  Lemma cancel_local_update x y z `{!Cancelable x} :
+    (x â‹… y, x â‹… z) ~l~> (y, z).
+  Proof.
+    intros ? f ? Heq. split; first by eapply cmra_validN_op_r.
+    apply (cancelableN x); first done. by rewrite -cmra_opM_assoc.
+  Qed.
+
   Lemma local_update_discrete `{!CMRADiscrete A} (x y x' y' : A) :
     (x,y) ~l~> (x',y') ↔ ∀ mz, ✓ x → x ≡ y ⋅? mz → ✓ x' ∧ x' ≡ y' ⋅? mz.
   Proof.
@@ -109,6 +116,12 @@ Section updates_unital.
     - intros Hup [z|]; simpl; [by auto|].
       rewrite -(right_id ∅ op y) -(right_id ∅ op y'). auto.
   Qed.
+
+  Lemma cancel_local_update_empty x y `{!Cancelable x} :
+    (x ⋅ y, x) ~l~> (y, ∅).
+  Proof.
+    rewrite -{2}(right_id ∅ op x). by apply cancel_local_update.
+  Qed.
 End updates_unital.
 
 (** * Product *)