diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index e938f99eb6e3be9ead8a7027a481bb523f61aea0..de8f9c2d32a5a86cb8e70af1176fbafe76cca1cf 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1068,7 +1068,7 @@ Section map2.
       naive_solver.
   Qed.
 
-  Lemma big_sepM2_fmap {A' B'} (f : A â†’ A') (g : B â†’ B') (Î¦ : nat â†’ A' â†’ B' â†’ PROP) m1 m2 :
+  Lemma big_sepM2_fmap {A' B'} (f : A â†’ A') (g : B â†’ B') (Î¦ : K â†’ A' â†’ B' â†’ PROP) m1 m2 :
     ([âˆ— map] kâ†¦y1;y2 âˆˆ f <$> m1; g <$> m2, Î¦ k y1 y2)
     âŠ£âŠ¢ ([âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦ k (f y1) (g y2)).
   Proof.
@@ -1082,12 +1082,12 @@ Section map2.
     - by rewrite big_sepM_fmap.
   Qed.
 
-  Lemma big_sepM2_fmap_l {A'} (f : A â†’ A') (Î¦ : nat â†’ A' â†’ B â†’ PROP) m1 m2 :
+  Lemma big_sepM2_fmap_l {A'} (f : A â†’ A') (Î¦ : K â†’ A' â†’ B â†’ PROP) m1 m2 :
     ([âˆ— map] kâ†¦y1;y2 âˆˆ f <$> m1; m2, Î¦ k y1 y2)
     âŠ£âŠ¢ ([âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦ k (f y1) y2).
   Proof. rewrite -{1}(map_fmap_id m2). apply big_sepM2_fmap. Qed.
 
-  Lemma big_sepM2_fmap_r {B'} (g : B â†’ B') (Î¦ : nat â†’ A â†’ B' â†’ PROP) m1 m2 :
+  Lemma big_sepM2_fmap_r {B'} (g : B â†’ B') (Î¦ : K â†’ A â†’ B' â†’ PROP) m1 m2 :
     ([âˆ— map] kâ†¦y1;y2 âˆˆ m1; g <$> m2, Î¦ k y1 y2)
     âŠ£âŠ¢ ([âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦ k y1 (g y2)).
   Proof. rewrite -{1}(map_fmap_id m1). apply big_sepM2_fmap. Qed.