From cd6ed5969e87896c9d4353ae49ae422b8b6bba59 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 7 Aug 2016 12:43:57 +0200
Subject: [PATCH] Simplify now_True_rvs.

---
 algebra/upred.v             | 2 +-
 proofmode/class_instances.v | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 1bd35b4c9..d15db3354 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1244,7 +1244,7 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma now_True_rvs P : ◇ (|=r=> ◇ P) ⊢ (|=r=> ◇ P).
+Lemma now_True_rvs P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).
 Proof.
   rewrite /uPred_now_True. apply or_elim; auto using rvs_mono.
   by rewrite -rvs_intro -or_intro_l.
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 988f33754..3f0fbc015 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -340,7 +340,8 @@ Global Instance is_now_True_later P : IsNowTrue (â–· P).
 Proof. by rewrite /IsNowTrue now_True_later. Qed.
 Global Instance is_now_True_rvs P : IsNowTrue P → IsNowTrue (|=r=> P).
 Proof.
-  rewrite /IsNowTrue=> HP. by rewrite -{2}HP -now_True_rvs -(now_True_intro P).
+  rewrite /IsNowTrue=> HP.
+  by rewrite -{2}HP -(now_True_idemp P) -now_True_rvs -(now_True_intro P).
 Qed.
 
 (* FromViewShift *)
-- 
GitLab