From 452bcbc66a4a756cfba23352442afe9f9a5c9384 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 16 Jan 2021 19:02:21 +0100
Subject: [PATCH] rename new lemma to big_sepL_sepL2

---
 iris/bi/big_op.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 46d6f7f7c..9477b7465 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) -∗
-- 
GitLab