diff --git a/algebra/gset.v b/algebra/gset.v
index 06fd34e7da95fd3a81fd40623fae858378a2560d..8701a4744253d71fe835405fd2a319b47b9ec3bd 100644
--- a/algebra/gset.v
+++ b/algebra/gset.v
@@ -74,4 +74,13 @@ Section gset.
   Proof. eauto using updateP_alloc_strong. Qed.
   Lemma updateP_alloc' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
   Proof. eauto using updateP_alloc. Qed.
+
+  Lemma alloc_singleton_local_update X i Xf :
+    i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).
+  Proof.
+    intros ??; apply local_update_total; split; simpl.
+    - rewrite !gset_disj_valid_op; set_solver.
+    - intros mZ ?%gset_disj_valid_op HXf.
+      rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
+  Qed.
 End gset.