From bfbc4420da96134454f30be2296f73e8cc557fbe Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 14 Feb 2016 09:58:42 +0100
Subject: [PATCH] prove compatibility of later and iff

---
 algebra/upred.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/algebra/upred.v b/algebra/upred.v
index e6bd3aefb..3910a66c6 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -710,6 +710,8 @@ Proof.
 Qed.
 Lemma later_wand P Q : ▷ (P -★ Q) ⊑ (▷ P -★ ▷ Q).
 Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
+Lemma later_iff P Q : (▷ (P ↔ Q)) ⊑ (▷P ↔ ▷Q).
+Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 Lemma löb_all_1 {A} (P Q : A → uPred M) :
   (∀ a, (▷(∀ b, P b → Q b) ∧ P a) ⊑ Q a) → ∀ a, P a ⊑ Q a.
 Proof.
-- 
GitLab