From 1ded5657a0055b50c2d4c5a3baa5880ec9de07c3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Jul 2016 17:16:48 +0200
Subject: [PATCH] Rule for eliminating a raw view shift into a pure
 proposition.

---
 algebra/upred.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/algebra/upred.v b/algebra/upred.v
index 98051ea3b..643e5df77 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).
-- 
GitLab