diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index e7b702f290ecdd70a65db7c8e2989a21d0c45597..8f29847b1569607e6da81da14ec46bbfa06625f1 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -743,19 +743,19 @@ Section sep_list2.
     by rewrite IH.
   Qed.
 
-  Lemma big_sepL_sepL2 (Î¦1 : nat â†’ A â†’ PROP) (Î¦2 : nat â†’ B â†’ PROP) l1 l2 :
+  Lemma big_sepL2_sepL (Î¦1 : nat â†’ A â†’ PROP) (Î¦2 : nat â†’ B â†’ PROP) l1 l2 :
     length l1 = length l2 â†’
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¦1 k y1 âˆ— Î¦2 k y2) âŠ£âŠ¢
     ([âˆ— list] kâ†¦y1 âˆˆ l1, Î¦1 k y1) âˆ— ([âˆ— list] kâ†¦y2 âˆˆ l2, Î¦2 k y2).
   Proof.
     intros. rewrite -big_sepL_sep_zip // big_sepL2_alt pure_True // left_id //.
   Qed.
-  Lemma big_sepL_sepL2_2 (Î¦1 : nat â†’ A â†’ PROP) (Î¦2 : nat â†’ B â†’ PROP) l1 l2 :
+  Lemma big_sepL2_sepL_2 (Î¦1 : nat â†’ A â†’ PROP) (Î¦2 : nat â†’ B â†’ PROP) l1 l2 :
     length l1 = length l2 â†’
     ([âˆ— list] kâ†¦y1 âˆˆ l1, Î¦1 k y1) -âˆ—
     ([âˆ— list] kâ†¦y2 âˆˆ l2, Î¦2 k y2) -âˆ—
     [âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¦1 k y1 âˆ— Î¦2 k y2.
-  Proof. intros. apply wand_intro_r. by rewrite big_sepL_sepL2. Qed.
+  Proof. intros. apply wand_intro_r. by rewrite big_sepL2_sepL. Qed.
 
   Global Instance big_sepL2_nil_persistent Î¦ :
     Persistent ([âˆ— list] kâ†¦y1;y2 âˆˆ []; [], Î¦ k y1 y2).
@@ -1715,19 +1715,19 @@ Section map2.
     apply big_sepM2_mono. eauto.
   Qed.
 
-  Lemma big_sepM_sepM2 (Î¦1 : K â†’ A â†’ PROP) (Î¦2 : K â†’ B â†’ PROP) m1 m2 :
+  Lemma big_sepM2_sepM (Î¦1 : K â†’ A â†’ PROP) (Î¦2 : K â†’ B â†’ PROP) m1 m2 :
     (âˆ€ k, is_Some (m1 !! k) â†” is_Some (m2 !! k)) â†’
     ([âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦1 k y1 âˆ— Î¦2 k y2) âŠ£âŠ¢
     ([âˆ— map] kâ†¦y1 âˆˆ m1, Î¦1 k y1) âˆ— ([âˆ— map] kâ†¦y2 âˆˆ m2, Î¦2 k y2).
   Proof.
     intros. rewrite -big_sepM_sep_zip // big_sepM2_alt pure_True // left_id //.
   Qed.
-  Lemma big_sepM_sepM2_2 (Î¦1 : K â†’ A â†’ PROP) (Î¦2 : K â†’ B â†’ PROP) m1 m2 :
+  Lemma big_sepM2_sepM_2 (Î¦1 : K â†’ A â†’ PROP) (Î¦2 : K â†’ B â†’ PROP) m1 m2 :
     (âˆ€ k, is_Some (m1 !! k) â†” is_Some (m2 !! k)) â†’
     ([âˆ— map] kâ†¦y1 âˆˆ m1, Î¦1 k y1) -âˆ—
     ([âˆ— map] kâ†¦y2 âˆˆ m2, Î¦2 k y2) -âˆ—
     [âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦1 k y1 âˆ— Î¦2 k y2.
-  Proof. intros. apply wand_intro_r. by rewrite big_sepM_sepM2. Qed.
+  Proof. intros. apply wand_intro_r. by rewrite big_sepM2_sepM. Qed.
 
   Global Instance big_sepM2_empty_persistent Î¦ :
     Persistent ([âˆ— map] kâ†¦y1;y2 âˆˆ âˆ…; âˆ…, Î¦ k y1 y2).