Big op over set union.

algebra/cmra_big_op.v

@@ -378,6 +378,16 @@ Section gset.
     x ∉ X → ([⋅ set] y ∈ {[ x ]} ∪ X, <[x:=P]> f y) ≡ (P ⋅ [⋅ set] y ∈ X, f y).
   Proof. apply (big_opS_fn_insert (λ y, id)). Qed.
 
+  Lemma big_opS_union f X Y :
+    X ⊥ Y →
+    ([⋅ set] y ∈ X ∪ Y, f y) ≡ ([⋅ set] y ∈ X, f y) ⋅ ([⋅ set] y ∈ Y, f y).
+  Proof.
+    intros. induction X as [|x X ? IH] using collection_ind_L.
+    { by rewrite left_id_L big_opS_empty left_id. }
+    rewrite -assoc_L !big_opS_insert; [|set_solver..].
+    by rewrite -assoc IH; last set_solver.
+  Qed.
+
   Lemma big_opS_delete f X x :
     x ∈ X → ([⋅ set] y ∈ X, f y) ≡ f x ⋅ [⋅ set] y ∈ X ∖ {[ x ]}, f y.
   Proof.

base_logic/big_op.v

@@ -457,6 +457,11 @@ Section gset.
     x ∉ X → ([∗ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ∗ [∗ set] y ∈ X, Φ y).
   Proof. apply: big_opS_fn_insert'. Qed.
 
+  Lemma big_sepS_union Φ X Y :
+    X ⊥ Y →
+    ([∗ set] y ∈ X ∪ Y, Φ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ Y, Φ y).
+  Proof. apply: big_opS_union. Qed.
+
   Lemma big_sepS_delete Φ X x :
     x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y.
   Proof. apply: big_opS_delete. Qed.