From 2a4e4330140df1e166edf5bcaccb280ca171125e Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sun, 14 Jul 2019 12:03:29 +0200
Subject: [PATCH] Rename `big_sepL2_app_inv_2` -> `big_sepL2_app_inv`.

And shorten the proof.
---
 theories/bi/big_op.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index bd7fb0fd7..221dd24a6 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -335,6 +335,16 @@ Section sep_list2.
        [by rewrite left_id|by rewrite left_id|apply False_elim|].
     by rewrite IH -assoc.
   Qed.
+  Lemma big_sepL2_app_inv Φ l1 l2 l1' l2' :
+    length l1 = length l1' →
+    ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2) -∗
+    ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) ∗
+    ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k)%nat y1 y2).
+  Proof.
+    revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] //= ?; simplify_eq.
+    - by rewrite left_id.
+    - by rewrite -assoc IH.
+  Qed.
 
   Lemma big_sepL2_mono Φ Ψ l1 l2 :
     (∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → Φ k y1 y2 ⊢ Ψ k y1 y2) →
-- 
GitLab