From dba0b4798cd9f51c3d2b2c6487b5386cac0b461f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 2 Dec 2016 10:58:53 +0100
Subject: [PATCH] Introduction of stepping fancy updates.
---
base_logic/lib/fancy_updates.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index f9540df97..ccb17becf 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -224,4 +224,7 @@ Proof.
iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
Qed.
+
+Lemma step_fupd_intro E1 E2 P : E2 ⊆ E1 → ▷ P -∗ |={E1,E2}▷=> P.
+Proof. iIntros (?) "HP". iApply (step_fupd_mask_mono E2 _ _ E2); auto. Qed.
End step_fupd.
--
GitLab