diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index d6eaeb4965abfef957459c8e94e2d9abd375fdfc..22ef7853ec2296e511ea771cda0668fbeb0431b1 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -650,6 +650,14 @@ Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opM_commute. by apply big_sepM_mono.
 Qed.
+Global Instance into_laterN_big_sepM2 n `{Countable K} {A}
+    (Φ Ψ : K → A → A → PROP) (m1 m2 : gmap K A) :
+  (∀ x1 x2 k, IntoLaterN false n (Φ k x1 x2) (Ψ k x1 x2)) →
+  IntoLaterN false n ([∗ map] k ↦ x1;x2 ∈ m1;m2, Φ k x1 x2) ([∗ map] k ↦ x1;x2 ∈ m1;m2, Ψ k x1 x2).
+Proof.
+  rewrite /IntoLaterN /MaybeIntoLaterN=> HΦΨ.
+  rewrite -big_sepM2_laterN_2. by apply big_sepM2_mono.
+Qed.
 Global Instance into_laterN_big_sepS n `{Countable A}
     (Φ Ψ : A → PROP) (X : gset A) :
   (∀ x, IntoLaterN false n (Φ x) (Ψ x)) →
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index cf2661ddd673845e0130de4d1c57ead057bdb81e..52b46c8302e631a6e833c1071d41157ead18075d 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -2414,6 +2414,8 @@ Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
   rewrite envs_entails_eq; apply big_sepL2_nil' : core.
 Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
   rewrite envs_entails_eq; apply big_sepM_empty' : core.
+Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
+  rewrite envs_entails_eq; apply big_sepM2_empty' : core.
 Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
   rewrite envs_entails_eq; apply big_sepS_empty' : core.
 Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>