From a9b6aa75491c75dfe8db91c4b0c0fb1a241f65d8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 6 Mar 2020 17:14:15 +0100
Subject: [PATCH] prove later commuting around equality one way

---
 theories/bi/derived_laws_sbi.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 9953ed04b..3dd19b1db 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -167,6 +167,12 @@ Qed.
 
 Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
 Proof. apply (anti_symm _); auto using later_eq_1, later_eq_2. Qed.
+Lemma later_equivI_prop (P Q : PROP) : ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
+Proof.
+  move: (@later_contractive PROP)=> /contractive_alt [g [? Hlt]].
+  rewrite (Hlt P) (Hlt Q) -later_equivI.
+  eapply (internal_eq_rewrite' (Next P) (Next Q) (λ Qx, g (Next P) ≡ g Qx)%I); auto.
+Qed.
 
 (* Later derived *)
 Hint Resolve later_mono : core.
-- 
GitLab