diff --git a/theories/gmap.v b/theories/gmap.v
index 9b49181e25bfa288ea31a9e22d947d7e0939e256..256b05e9ba77ee5d317d33f5404459cdba524ed8 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -286,6 +286,11 @@ Section gset.
   (** If you are looking for a lemma showing that [gset] is extensional, see
   [sets.set_eq]. *)
 
+  (** The function [gset_to_gmap x X] converts a set [X] to a map with domain
+  [X] where each key has value [x]. Compared to the generic conversion
+  [set_to_map], the function [gset_to_gmap] has [O(n)] instead of [O(n log n)]
+  complexity and has an easier and better developed theory. *)
+
   Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
     (λ _, x) <$> mapset_car X.
 
@@ -342,6 +347,13 @@ Section gset.
     - rewrite gset_to_gmap_empty, dom_empty_L; done.
     - rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
   Qed.
+
+  Lemma gset_to_gmap_set_to_map {A} (X : gset K) (x : A) :
+    gset_to_gmap x X = set_to_map (.,x) X.
+  Proof.
+    apply map_eq; intros k. apply option_eq; intros y.
+    rewrite lookup_gset_to_gmap_Some, lookup_set_to_map; naive_solver.
+  Qed.
 End gset.
 
 Typeclasses Opaque gset.