From eb200cc0d13ca98823d11094de8c9f070565ffbb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 Mar 2020 21:33:43 +0100
Subject: [PATCH] Add lemma `fupd_plain_laterN`.

---
 theories/bi/updates.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 7679b2924..1c3ecec3b 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -430,6 +430,12 @@ Section fupd_derived.
 
     Lemma fupd_plain_later E P `{!Plain P} : (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
     Proof. by rewrite {1}(plain P) fupd_plainly_later. Qed.
+    Lemma fupd_plain_laterN E n P `{!Plain P} : (▷^n |={E}=> P) ⊢ |={E}=> ▷^n ◇ P.
+    Proof.
+      induction n as [|n IH]; simpl; [by rewrite -except_0_intro|].
+      by rewrite IH fupd_plain_later except_0_laterN except_0_idemp.
+    Qed.
+
     Lemma fupd_plain_forall_2 E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
       (∀ x, |={E}=> Φ x) ⊢ |={E}=> ∀ x, Φ x.
     Proof.
-- 
GitLab