From 175ae7e683386e5f212284deea16155bf1a0aa68 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 00:40:23 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20(P=20=E2=89=A1=20Q)=20=E2=8A=A2=20(P=20?=
 =?UTF-8?q?=E2=86=94=20Q).?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/algebra/upred.v b/algebra/upred.v
index a354f58b1..33a7afb0a 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -683,6 +683,7 @@ Lemma const_elim_r φ Q R : (φ → Q ⊢ R) → (Q ∧ ■ φ) ⊢ R.
 Proof. intros; apply const_elim with φ; eauto. Qed.
 Lemma const_equiv (φ : Prop) : φ → (■ φ) ⊣⊢ True.
 Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
+
 Lemma eq_refl' {A : cofeT} (a : A) P : P ⊢ (a ≡ a).
 Proof. rewrite (True_intro P). apply eq_refl. Qed.
 Hint Resolve eq_refl'.
@@ -690,6 +691,10 @@ Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ (a ≡ b).
 Proof. by intros ->. Qed.
 Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊢ (b ≡ a).
 Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed.
+Lemma eq_iff P Q : (P ≡ Q) ⊢ (P ↔ Q).
+Proof.
+  apply (eq_rewrite P Q (λ Q, P ↔ Q))%I; first solve_proper; auto using iff_refl.
+Qed.
 
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : P ⊢ Q → P' ⊢ Q' → (P ★ P') ⊢ (Q ★ Q').
-- 
GitLab