diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 46d6f7f7cb382dc72289e271b7369e8cf7914caa..9477b7465e9257fc498b3b53e264ef64c7666d4c 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -645,7 +645,7 @@ Section sep_list2.
     by rewrite IH.
   Qed.
 
-  Lemma big_sepL2_merge (Φ : nat → A → PROP) (Ψ : nat → B → PROP)
+  Lemma big_sepL_sepL2 (Φ : nat → A → PROP) (Ψ : nat → B → PROP)
       (l1 : list A) (l2 : list B) :
     length l1 = length l2 →
     ([∗ list] k↦y1 ∈ l1, Φ k y1) -∗