From 790f7f331e5e48e1c3a698515ee48fb2b016ab46 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 17 Jan 2021 12:06:56 +0100
Subject: [PATCH] Move header to the right place.

---
 iris/bi/big_op.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 83fead25d..c1ffa2d50 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -319,9 +319,10 @@ Proof.
   - by rewrite IH.
 Qed.
 
+(** ** Big ops over two lists *)
 Lemma big_sepL2_alt {A B} (Φ : nat → A → B → PROP) l1 l2 :
-  ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2)
-  ⊣⊢ ⌜ length l1 = length l2 ⌝ ∧ [∗ list] k ↦ y ∈ zip l1 l2, Φ k (y.1) (y.2).
+  ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2) ⊣⊢
+  ⌜ length l1 = length l2 ⌝ ∧ [∗ list] k ↦ xy ∈ zip l1 l2, Φ k (xy.1) (xy.2).
 Proof.
   apply (anti_symm _).
   - apply and_intro.
@@ -335,7 +336,6 @@ Proof.
     induction Hl as [|x1 l1 x2 l2 _ _ IH]=> Φ //=. by rewrite -IH.
 Qed.
 
-(** ** Big ops over two lists *)
 Section sep_list2.
   Context {A B : Type}.
   Implicit Types Φ Ψ : nat → A → B → PROP.
-- 
GitLab