From c69907558945f052be28a039ac53eaf7f46c92fe Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 27 Apr 2023 10:52:01 +0200
Subject: [PATCH] Generalize `intuitionistically_intro` to general BI.

---
 iris/bi/derived_laws.v | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index f0a857148..7dde67cb7 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1632,14 +1632,12 @@ would be its only field. *)
 Lemma intuitionistic P `{!Persistent P, !Affine P} : P ⊢ □ P.
 Proof. rewrite intuitionistic_intuitionistically. done. Qed.
 
+Lemma intuitionistically_intro P Q `{!Affine P, !Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
+Proof. intros. apply: affinely_intro. by apply: persistently_intro. Qed.
+
 Section persistent_bi_absorbing.
   Context `{!BiAffine PROP}.
 
-  Lemma intuitionistically_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
-  Proof.
-    intros HP. rewrite (persistent P) HP intuitionistically_into_persistently //.
-  Qed.
-
   Lemma persistent_and_sep P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
     P ∧ Q ⊣⊢ P ∗ Q.
   Proof.
-- 
GitLab