diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index cc13f1972e98195cd51eb052ae3fb039e91276fc..b4c2bf994098f9e66d4d67c884db37c70f20fe9e 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -591,6 +591,11 @@ Proof.
   apply wand_elim_l', big_sepL2_app.
 Qed.
 
+Global Instance from_and_big_sepMS_union_persistent `{Countable A} (Φ : A → PROP) X1 X2 :
+  (∀ y, Persistent (Φ y)) →
+  FromAnd ([∗ mset] y ∈ X1 ∪ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
+Proof. intros. by rewrite /FromAnd big_sepMS_union persistent_and_sep_1. Qed.
+
 (** FromSep *)
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
 Proof. by rewrite /FromSep. Qed.
@@ -644,6 +649,10 @@ Global Instance from_sep_big_sepL2_app {A B} (Φ : nat → A → B → PROP)
     ([∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
 Proof. rewrite /IsApp=>-> ->. apply wand_elim_l', big_sepL2_app. Qed.
 
+Global Instance from_sep_big_sepMS_union `{Countable A} (Φ : A → PROP) X1 X2 :
+  FromSep ([∗ mset] y ∈ X1 ∪ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
+Proof. by rewrite /FromSep big_sepMS_union. Qed.
+
 Global Instance from_sep_bupd `{BiBUpd PROP} P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
@@ -793,6 +802,10 @@ Global Instance into_sep_big_sepL2_cons {A B}
     (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
 Proof. rewrite /IsCons=>-> ->. by rewrite /IntoSep big_sepL2_cons. Qed.
 
+Global Instance into_sep_big_sepMS_union `{Countable A} (Φ : A → PROP) X1 X2 :
+  IntoSep ([∗ mset] y ∈ X1 ∪ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
+Proof. by rewrite /IntoSep big_sepMS_union. Qed.
+
 (** FromOr *)
 Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
 Proof. by rewrite /FromOr. Qed.
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 3dee777bfa9cbfb8c15a6ac6587e29da4bd42b1e..9a5c852043f724e7caba86485f5c055416f6680e 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -105,6 +105,11 @@ Global Instance frame_big_sepL2_app {A B} p (Φ : nat → A → B → PROP)
   Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
 Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.
 
+Global Instance frame_big_sepMS_union `{Countable A} p (Φ : A → PROP) R Q X1 X2 :
+  Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
+  Frame p R ([∗ mset] y ∈ X1 ∪ X2, Φ y) Q.
+Proof. by rewrite /Frame big_sepMS_union. Qed.
+
 Global Instance make_and_true_l P : KnownLMakeAnd True P P.
 Proof. apply left_id, _. Qed.
 Global Instance make_and_true_r P : KnownRMakeAnd P True P.