diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index f2fb0cbd9650ca9244543ea3c0c9df5aa4a0db2e..7c1c6167e726dd1051f20bfd7f393f82b79cf9ac 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1437,9 +1437,8 @@ Section gmap.
 End gmap.
 
 Section gmap2.
-  Context `{Countable K} {A : Type}.
-  Implicit Types m : gmap K A.
-  Implicit Types Φ Ψ : K → A → A → PROP.
+  Context `{Countable K} {A B : Type}.
+  Implicit Types Φ Ψ : K → A → B → PROP.
 
   Lemma big_sepM2_later_1 `{BiAffine PROP} Φ m1 m2 :
     (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 22ef7853ec2296e511ea771cda0668fbeb0431b1..b23e54df1be72188c71d5f8c59d694cca4fd1736 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -650,8 +650,8 @@ 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) :
+Global Instance into_laterN_big_sepM2 n `{Countable K} {A B}
+    (Φ Ψ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) :
   (∀ 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.