From b433bf120531cc532ff76883cec683229bcfe0ee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 May 2020 16:54:08 +0200
Subject: [PATCH] =?UTF-8?q?Add=20lemma=20`intuitionistically=5Fimpl=5Fwand?=
 =?UTF-8?q?=5F2=20P=20Q=20:=20=E2=96=A1=20(P=20-=E2=88=97=20Q)=20=E2=8A=A2?=
 =?UTF-8?q?=20=E2=96=A1=20(P=20=E2=86=92=20Q)`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This lemma is similar to `persistently_impl_wand_2`.
---
 theories/bi/derived_laws.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 40641c9b9..2a1bbc107 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1094,6 +1094,9 @@ Proof.
     apply sep_mono; first done. apply and_elim_r.
 Qed.
 
+Lemma intuitionistically_impl_wand_2 P Q : □ (P -∗ Q) ⊢ □ (P → Q).
+Proof. by rewrite /bi_intuitionistically persistently_impl_wand_2. Qed.
+
 Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q).
 Proof.
   apply (anti_symm (⊢)).
-- 
GitLab