From 92326ed3c31c237f6d68441b888c591cb77fae8d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Feb 2016 18:42:25 +0100
Subject: [PATCH] uPred_equiv is reflexive.

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

diff --git a/algebra/upred.v b/algebra/upred.v
index c01128510..e6bd3aefb 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -521,6 +521,9 @@ Proof.
   * by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
   * by apply impl_intro_l; rewrite left_id.
 Qed.
+Lemma iff_refl Q P : Q ⊑ (P ↔ P).
+Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
+
 Lemma or_and_l P Q R : (P ∨ Q ∧ R)%I ≡ ((P ∨ Q) ∧ (P ∨ R))%I.
 Proof.
   apply (anti_symm (⊑)); first auto.
@@ -832,7 +835,6 @@ Proof. done. Qed.
 Lemma prod_validI {A B : cmraT} (x : A * B) :
   (✓ x)%I ≡ (✓ x.1 ∧ ✓ x.2 : uPred M)%I.
 Proof. done. Qed.
-Print later.
 Lemma later_equivI {A : cofeT} (x y : later A) :
   (x ≡ y)%I ≡ (▷ (later_car x ≡ later_car y) : uPred M)%I.
 Proof. done. Qed.
@@ -1001,5 +1003,5 @@ Hint Resolve and_intro and_elim_l' and_elim_r' : I.
 Hint Resolve always_mono : I.
 Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
 Hint Immediate True_intro False_elim : I.
-
+Hint Immediate iff_refl : I.
 End uPred.
-- 
GitLab