diff --git a/algebra/gset.v b/algebra/gset.v
index 1ee25c530e536cb01ec33ff3b8b265f4327715d6..8cc7816168cf6413cd6407b2b2068420272a5766 100644
--- a/algebra/gset.v
+++ b/algebra/gset.v
@@ -174,6 +174,23 @@ Section gset_disj.
     Proof. eauto using gset_disj_alloc_empty_updateP. Qed.
   End fresh_updates.
 
+  Lemma gset_disj_dealloc_local_update X Y Xf :
+    GSet X ~l~> GSet (X ∖ Y) @ Some (GSet Xf).
+  Proof.
+    apply local_update_total; split; simpl.
+    { rewrite !gset_disj_valid_op; set_solver. }
+    intros mZ ?%gset_disj_valid_op. rewrite gset_disj_union //.
+    destruct mZ as [[Z|]|]; simpl; try done.
+    - rewrite {1}/op {1}/cmra_op /=. destruct (decide _); simpl; try done.
+      intros [=]. do 2 f_equal. by apply union_cancel_l_L with X.
+    - intros [=]. assert (Xf = ∅) as -> by set_solver. by rewrite right_id.
+  Qed.
+  Lemma gset_disj_dealloc_empty_local_update X Xf :
+    GSet X ~l~> GSet ∅ @ Some (GSet Xf).
+  Proof.
+    rewrite -(difference_diag_L X). apply gset_disj_dealloc_local_update.
+  Qed.
+
   Lemma gset_disj_alloc_local_update X i Xf :
     i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).
   Proof.