From ceee71053e43fa2902d557db86627f5cf7306197 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Mar 2018 18:06:12 +0100
Subject: [PATCH] show that persistently is also another fixpoint

---
 theories/bi/derived_laws.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 8da81d331..d60d9a75e 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -850,6 +850,12 @@ Proof.
   - rewrite comm persistently_absorbing. done.
 Qed.
 
+Lemma persistently_alt_fixpoint' P :
+  <pers> P âŠ£âŠ¢ <affine> P âˆ— <pers> P.
+Proof.
+  rewrite -{1}persistently_affinely {1}persistently_alt_fixpoint persistently_affinely //.
+Qed.
+
 Lemma persistently_wand P Q : <pers> (P -âˆ— Q) âŠ¢ <pers> P -âˆ— <pers> Q.
 Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
 
-- 
GitLab