diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 2fa14e8eed6645bf451f29425e391d87fae1cdb8..8edbfb7e2d730f4e9ee4a35b8df1d80f91b2fa4a 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -672,6 +672,21 @@ Proof.
   rewrite insert_singleton_op ?not_elem_of_list_to_map_1 //.
 Qed.
 
+Lemma big_opS_gset_to_gmap (X : gset K) (a : A) :
+  ([^op set] x ∈ X, {[ x := a ]}) ≡ gset_to_gmap a X.
+Proof.
+  induction X as [|? ? ? IHX] using set_ind_L.
+  { intros ?; rewrite big_opS_empty gset_to_gmap_empty //=. }
+  rewrite big_opS_insert //.
+  rewrite gset_to_gmap_union_singleton.
+  rewrite insert_singleton_op; [|by rewrite lookup_gset_to_gmap_None].
+  by rewrite IHX.
+Qed.
+
+Lemma big_opS_gset_to_gmap_L `{!LeibnizEquiv A} (X : gset K) (a : A) :
+  ([^op set] x ∈ X, {[ x := a ]}) = gset_to_gmap a X.
+Proof. apply leibniz_equiv, big_opS_gset_to_gmap. Qed.
+
 End properties.
 
 Section unital_properties.