From b31d8c00221f2cc4fb53f657ad9bb881a95b74da Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 13 May 2020 20:28:04 +0200
Subject: [PATCH] Add big_sepL2_nil_inv_l/r.

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

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 4c702da91..21cd47aac 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -292,6 +292,12 @@ Section sep_list2.
   Proof. done. Qed.
   Lemma big_sepL2_nil' `{BiAffine PROP} P Φ : P ⊢ [∗ list] k↦y1;y2 ∈ [];[], Φ k y1 y2.
   Proof. apply (affine _). Qed.
+  Lemma big_sepL2_nil_inv_l Φ l2 :
+    ([∗ list] k↦y1;y2 ∈ []; l2, Φ k y1 y2) -∗ ⌜l2 = []⌝.
+  Proof. destruct l2; simpl; auto using False_elim, pure_intro. Qed.
+  Lemma big_sepL2_nil_inv_r Φ l1 :
+    ([∗ list] k↦y1;y2 ∈ l1; [], Φ k y1 y2) -∗ ⌜l1 = []⌝.
+  Proof. destruct l1; simpl; auto using False_elim, pure_intro. Qed.
 
   Lemma big_sepL2_cons Φ x1 x2 l1 l2 :
     ([∗ list] k↦y1;y2 ∈ x1 :: l1; x2 :: l2, Φ k y1 y2)
-- 
GitLab