diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index a46cfcd9b77df3d417ef9f5da3bd35ab24b10818..f2fb0cbd9650ca9244543ea3c0c9df5aa4a0db2e 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1436,6 +1436,62 @@ Section gmap.
   End plainly.
 End gmap.
 
+Section gmap2.
+  Context `{Countable K} {A : Type}.
+  Implicit Types m : gmap K A.
+  Implicit Types Φ Ψ : K → A → A → PROP.
+
+  Lemma big_sepM2_later_1 `{BiAffine PROP} Φ m1 m2 :
+    (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
+    ⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
+  Proof.
+    rewrite /big_sepM2 later_and (timeless ⌜_⌝%I).
+    rewrite big_sepM_later except_0_and.
+    auto using and_mono_r, except_0_intro.
+  Qed.
+  Lemma big_sepM2_later_2 Φ m1 m2 :
+    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2)
+    ⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
+  Proof.
+    rewrite /big_sepM2 later_and -(later_intro ⌜_⌝%I).
+    apply and_mono_r. by rewrite big_opM_commute.
+  Qed.
+
+  Lemma big_sepM2_laterN_2 Φ n m1 m2 :
+    ([∗ map] k↦x1;x2 ∈ m1;m2, ▷^n Φ k x1 x2)
+    ⊢ ▷^n [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
+  Proof.
+    induction n as [|n IHn]; first done.
+    rewrite later_laterN -IHn -big_sepM2_later_2.
+    apply big_sepM2_mono. eauto.
+  Qed.
+
+  Global Instance big_sepM2_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
+    Timeless ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
+  Proof. rewrite /big_sepM2 map_zip_with_empty. apply _. Qed.
+  Global Instance big_sepM2_timeless `{!Timeless (emp%I : PROP)} Φ m1 m2 :
+    (∀ k x1 x2, Timeless (Φ k x1 x2)) →
+    Timeless ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
+  Proof. intros. rewrite /big_sepM2. apply _. Qed.
+
+  Section plainly.
+    Context `{!BiPlainly PROP}.
+
+    Lemma big_sepM2_plainly `{BiAffine PROP} Φ m1 m2 :
+      ■ ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊣⊢
+      [∗ map] k↦x1;x2 ∈ m1;m2, ■ (Φ k x1 x2).
+    Proof. by rewrite /big_sepM2 plainly_and plainly_pure big_sepM_plainly. Qed.
+
+    Global Instance big_sepM2_empty_plain `{BiAffine PROP} Φ :
+      Plain ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
+    Proof. rewrite /big_sepM2 map_zip_with_empty. apply _. Qed.
+    Global Instance big_sepM2_plain `{BiAffine PROP} Φ m1 m2 :
+      (∀ k x1 x2, Plain (Φ k x1 x2)) →
+      Plain ([∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2).
+    Proof. intros. rewrite /big_sepM2. apply _. Qed.
+  End plainly.
+End gmap2.
+
 (** ** Big ops over finite sets *)
 Section gset.
   Context `{Countable A}.