From 584a9145ec7bac8dca7f8145e6d7f8c201cfb9a1 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 25 Jun 2019 20:40:02 +0200
Subject: [PATCH] Strengthen `lrel_list_cons`.

---
 theories/lib/list.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/lib/list.v b/theories/lib/list.v
index 72f7f4d..9f608a5 100644
--- a/theories/lib/list.v
+++ b/theories/lib/list.v
@@ -37,8 +37,8 @@ Proof.
 Qed.
 
 Lemma lrel_list_cons `{relocG Σ} (A : lrel Σ) v1 v2 ls1 ls2 :
-  A v1 v2 -∗
-  lrel_list A ls1 ls2 -∗
+  ▷ A v1 v2 -∗
+  ▷ lrel_list A ls1 ls2 -∗
   lrel_list A (CONSV v1 ls1) (CONSV v2 ls2).
 Proof.
   iIntros "#HA #Hls".
-- 
GitLab