diff --git a/theories/gmap.v b/theories/gmap.v
index 8684a92c0d89c92c733bd96cff5ef70d8383c669..3b0405e8ac2fb9a7abcd19c19a56bf295745a287 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -265,6 +265,13 @@ Section gset.
     rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
       elem_of_singleton; destruct (decide (i = j)); intuition.
   Qed.
+  Lemma gset_to_gmap_difference_singleton {A} (x : A) i Y :
+    gset_to_gmap x (Y ∖ {[i]}) = delete i (gset_to_gmap x Y).
+  Proof.
+    apply map_eq; intros j; apply option_eq; intros y.
+    rewrite lookup_delete_Some, !lookup_gset_to_gmap_Some, elem_of_difference,
+      elem_of_singleton; destruct (decide (i = j)); intuition.
+  Qed.
 
   Lemma fmap_gset_to_gmap {A B} (f : A → B) (X : gset K) (x : A) :
     f <$> gset_to_gmap x X = gset_to_gmap (f x) X.