diff --git a/algebra/upred.v b/algebra/upred.v
index 1bd35b4c9de6550b762a3a002cc779ce8a72e960..d15db33546f4fbecef4912b35791991adeb62d5d 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 988f337544dccec7128349279b1a7fc6eb0587a5..3f0fbc0151e9a3081a9b38dbfc0eb22fae948de8 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 *)