From ccfa119601270d7ea41c849cf920e175bc0887d8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Mar 2019 14:31:45 +0100
Subject: [PATCH] Add `big_sepL2_later_1`.

---
 theories/bi/big_op.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 9bef2299b..5aafb2212 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1027,6 +1027,13 @@ Section list2.
   Context {A B : Type}.
   Implicit Types Φ Ψ : nat → A → B → PROP.
 
+  Lemma big_sepL2_later_1 `{BiAffine PROP} Φ l1 l2 :
+    (▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ ◇ [∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2.
+  Proof.
+    rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ ⌝%I).
+    rewrite except_0_and. auto using and_mono, except_0_intro.
+  Qed.
+
   Lemma big_sepL2_later_2 Φ l1 l2 :
     ([∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2) ⊢ ▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
   Proof.
-- 
GitLab