diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index d973f58cfe8b285225e7553905e39e099509ca86..638ff303339e02b2f362033d2bb2cd1f323fd23d 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -492,12 +492,16 @@ Section gset.
     Proper (pointwise_relation _ (≡) ==> (=) ==> (≡)) (big_opS o (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opS_proper; intros; apply Hf. Qed.
 
+  Lemma big_opS_elements f X :
+    ([^o set] x ∈ X, f x) = [^o list] _↦x ∈ elements X, f x.
+  Proof. by rewrite big_opS_eq. Qed.
+
   Lemma big_opS_empty f : ([^o set] x ∈ ∅, f x) = monoid_unit.
-  Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
+  Proof. by rewrite big_opS_elements elements_empty. Qed.
 
   Lemma big_opS_insert f X x :
     x ∉ X → ([^o set] y ∈ {[ x ]} ∪ X, f y) ≡ (f x `o` [^o set] y ∈ X, f y).
-  Proof. intros. by rewrite big_opS_eq /big_opS_def elements_union_singleton. Qed.
+  Proof. intros. by rewrite !big_opS_elements elements_union_singleton. Qed.
   Lemma big_opS_fn_insert {B} (f : A → B → M) h X x b :
     x ∉ X →
     ([^o set] y ∈ {[ x ]} ∪ X, f y (<[x:=b]> h y))
@@ -529,7 +533,7 @@ Section gset.
   Qed.
 
   Lemma big_opS_singleton f x : ([^o set] y ∈ {[ x ]}, f y) ≡ f x.
-  Proof. intros. by rewrite big_opS_eq /big_opS_def elements_singleton /= right_id. Qed.
+  Proof. intros. by rewrite big_opS_elements elements_singleton /= right_id. Qed.
 
   Lemma big_opS_unit X : ([^o set] y ∈ X, monoid_unit) ≡ (monoid_unit : M).
   Proof.
@@ -552,7 +556,7 @@ Section gset.
 
   Lemma big_opS_op f g X :
     ([^o set] y ∈ X, f y `o` g y) ≡ ([^o set] y ∈ X, f y) `o` ([^o set] y ∈ X, g y).
-  Proof. by rewrite big_opS_eq /big_opS_def -big_opL_op. Qed.
+  Proof. by rewrite !big_opS_elements -big_opL_op. Qed.
 
   Lemma big_opS_list_to_set f (l : list A) :
     NoDup l →
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index be8823a1d5b97c37afd9f5a850b22ba8ce983b99..6209dbf57a6d79086b9d0dad24826adb1b68e5e9 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -357,6 +357,19 @@ Section sep_list.
 End sep_list.
 
 (* Some lemmas depend on the generalized versions of the above ones. *)
+Lemma big_sepL_sepL {A B : Type} (Φ : nat → A → nat → B → PROP) (l1 : list A) (l2 : list B) :
+  ([∗ list] k1↦x1 ∈ l1, [∗ list] k2↦x2 ∈ l2, Φ k1 x1 k2 x2) ⊣⊢
+  ([∗ list] k2↦x2 ∈ l2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 k2 x2).
+Proof.
+  revert Φ l2. induction l1 as [|x1 l1 IH]; intros Φ l2.
+  { rewrite big_sepL_nil. setoid_rewrite big_sepL_nil.
+    rewrite big_sepL_emp. done. }
+  rewrite big_sepL_cons.
+  setoid_rewrite big_sepL_cons.
+  rewrite big_sepL_sep. f_equiv.
+  rewrite IH //.
+Qed.
+
 Lemma big_sepL_sep_zip_with {A B C} (f : A → B → C) (g1 : C → A) (g2 : C → B)
     (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
   (∀ x y, g1 (f x y) = x) →
@@ -2010,6 +2023,10 @@ Section gset.
      Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
 
+  Lemma big_sepS_elements Φ X :
+    ([∗ set] x ∈ X, Φ x) ⊣⊢ [∗ list] _↦x ∈ elements X, Φ x.
+  Proof. by rewrite big_opS_elements. Qed.
+
   Lemma big_sepS_empty Φ : ([∗ set] x ∈ ∅, Φ x) ⊣⊢ emp.
   Proof. by rewrite big_opS_empty. Qed.
   Lemma big_sepS_empty' P `{!Affine P} Φ : P ⊢ [∗ set] x ∈ ∅, Φ x.
@@ -2232,6 +2249,14 @@ Section gset.
   Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
 End gset.
 
+Lemma big_sepS_sepS `{Countable A, Countable B}
+    (X : gset A) (Y : gset B) (Φ : A → B → PROP) :
+  ([∗ set] x ∈ X, [∗ set] y ∈ Y, Φ x y) -∗ ([∗ set] y ∈ Y, [∗ set] x ∈ X, Φ x y).
+Proof.
+  repeat setoid_rewrite big_sepS_elements.
+  rewrite big_sepL_sepL. done.
+Qed.
+
 Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) :
   ([∗ map] k↦_ ∈ m, Φ k) ⊣⊢ ([∗ set] k ∈ dom _ m, Φ k).
 Proof. apply big_opM_dom. Qed.