diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index cab92a41893b2db2c49468383d6ef8125a499a6f..bc89495ccad60f0c4c3b67ea101c0e75bb57a253 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -598,6 +598,22 @@ Proof.
   intros ??. rewrite !lookup_included=> Hm i.
   rewrite !lookup_fmap. by apply option_fmap_mono.
 Qed.
+
+Lemma big_opM_singletons m :
+  ([^op map] k ↦ x ∈ m, {[ k := x ]}) = m.
+Proof.
+  (* We are breaking the big_opM abstraction here. The reason is that [map_ind]
+     is too weak: we need an induction principle that visits all the keys in the
+     right order, namely the order in which they appear in map_to_list.  Here,
+     we achieve this by unfolding [big_opM] and doing induction over that list
+     instead. *)
+  rewrite big_opM_eq /big_opM_def -{2}(list_to_map_to_list m).
+  assert (NoDup (map_to_list m).*1) as Hnodup by apply NoDup_fst_map_to_list.
+  revert Hnodup. induction (map_to_list m) as [|[k x] l IH]; csimpl; first done.
+  intros [??]%NoDup_cons. rewrite IH //.
+  rewrite insert_singleton_op ?not_elem_of_list_to_map_1 //.
+Qed.
+
 End properties.
 
 Section unital_properties.
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 822a952e3156f2659266ee6fc354f9213db9bebc..4bbb9cf8de0cb7a9a0f5d2735813e01e37a39129 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -1,6 +1,6 @@
 From stdpp Require Export sets gmultiset countable.
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates.
+From iris.algebra Require Import updates local_updates big_op.
 From iris Require Import options.
 
 (* The multiset union CMRA *)
@@ -84,6 +84,15 @@ Section gmultiset.
     repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
     lia.
   Qed.
+
+  Lemma big_opMS_singletons X :
+    ([^op mset] x ∈ X, {[ x ]}) = X.
+  Proof.
+    induction X as [|x X IH] using gmultiset_ind.
+    - rewrite big_opMS_empty. done.
+    - unfold_leibniz. rewrite big_opMS_disj_union // big_opMS_singleton IH //.
+  Qed.
+
 End gmultiset.
 
 Arguments gmultisetO _ {_ _}.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index 5283498c8da39193a9db51426608c4decafc0c76..832616e9d59c972c8ed0f055b6643e11740f2d96 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -1,6 +1,6 @@
 From stdpp Require Export sets gmap mapset.
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates.
+From iris.algebra Require Import updates local_updates big_op.
 From iris Require Import options.
 
 (* The union CMRA *)
@@ -55,6 +55,15 @@ Section gset.
 
   Global Instance gset_core_id X : CoreId X.
   Proof. by apply core_id_total; rewrite gset_core_self. Qed.
+
+  Lemma big_opS_singletons X :
+    ([^op set] x ∈ X, {[ x ]}) = X.
+  Proof.
+    induction X as [|x X Hx IH] using set_ind_L.
+    - rewrite big_opS_empty. done.
+    - unfold_leibniz. rewrite big_opS_insert // IH //.
+  Qed.
+
 End gset.
 
 Arguments gsetO _ {_ _}.