From ec11ab9164eb7328109d6aa0a06130393305c822 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Feb 2016 20:50:04 +0100
Subject: [PATCH] Stronger saved_prop_agree with equality instead of iff.

---
 program_logic/saved_prop.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 96c2b8367..b2e8706a8 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -24,12 +24,12 @@ Section saved_prop.
   Proof. by apply own_alloc. Qed.
 
   Lemma saved_prop_agree γ P Q :
-    (saved_prop_own SPI γ P ★ saved_prop_own SPI γ Q) ⊑ ▷ (P ↔ Q).
+    (saved_prop_own SPI γ P ★ saved_prop_own SPI γ Q) ⊑ ▷ (P ≡ Q).
   Proof.
     rewrite /saved_prop_own -own_op own_valid agree_validI.
     rewrite agree_equivI later_equivI /=; apply later_mono.
     rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
     apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _,
-      iProp_fold (iProp_unfold P) ↔ iProp_fold Q')%I); solve_ne || auto with I.
+      iProp_fold (iProp_unfold P) ≡ iProp_fold Q')%I); solve_ne || auto with I.
   Qed.
 End saved_prop.
-- 
GitLab