Simplify now_True_rvs.

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.

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 *)