From 7a7e1d220d502f80601a1681de69efc21a194944 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 May 2018 23:47:57 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20`=E2=96=A1=20False=20=E2=8A=A3=E2=8A=A2?=
 =?UTF-8?q?=20False`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/derived_laws_bi.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index e62306783..1b5b013b5 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -988,6 +988,8 @@ Proof.
   by rewrite /bi_intuitionistically -persistently_True_emp persistently_pure
              affinely_True_emp affinely_emp.
 Qed.
+Lemma intuitionistically_False : □ False ⊣⊢ False.
+Proof. by rewrite /bi_intuitionistically persistently_pure affinely_False. Qed.
 Lemma intuitionistically_True_emp : □ True ⊣⊢ emp.
 Proof.
   rewrite -intuitionistically_emp /bi_intuitionistically
@@ -1179,6 +1181,8 @@ Proof. destruct p; simpl; auto using intuitionistically_intro'. Qed.
 
 Lemma intuitionistically_if_emp p : □?p emp ⊣⊢ emp.
 Proof. destruct p; simpl; auto using intuitionistically_emp. Qed.
+Lemma intuitionistically_if_False p : □?p False ⊣⊢ False.
+Proof. destruct p; simpl; auto using intuitionistically_False. Qed.
 Lemma intuitionistically_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
 Proof. destruct p; simpl; auto using intuitionistically_and. Qed.
 Lemma intuitionistically_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
-- 
GitLab