diff --git a/algebra/upred.v b/algebra/upred.v
index 98051ea3b32ae1e30ed424fed41ed05f0fd8d350..643e5df77fce9fd03e0c46b1bdcd7f33f90266a6 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1209,6 +1209,11 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
+Lemma rvs_later_pure φ : (|=r=> ▷ ■ φ) ⊢ ▷ ■ φ.
+Proof.
+  unseal; split=> -[|n] x ? Hvs; simpl in *; first done.
+  by destruct (Hvs (S n) (core x)) as (x'&?&?); [omega|by rewrite cmra_core_r|].
+Qed.
 
 (** * Derived rules *)
 Global Instance rvs_mono' : Proper ((⊢) ==> (⊢)) (@uPred_rvs M).