From b95c0bc7677747aa38d2644124df8df3e393d37b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 2 Jul 2016 12:02:29 +0200
Subject: [PATCH] Add lemma pure_iff.

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

diff --git a/algebra/upred.v b/algebra/upred.v
index 73d521139..607214971 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -564,6 +564,8 @@ Proof. intros ->; apply iff_refl. Qed.
 
 Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊢ ■ φ2.
 Proof. intros; apply pure_elim with φ1; eauto using pure_intro. Qed.
+Lemma pure_iff φ1 φ2 : (φ1 ↔ φ2) → ■ φ1 ⊣⊢ ■ φ2.
+Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
 Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
 Proof. auto. Qed.
 Lemma and_mono_l P P' Q : (P ⊢ Q) → P ∧ P' ⊢ Q ∧ P'.
-- 
GitLab