From 771b9aed548733ce81014b1a0734a0a0d433a1c3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 11 May 2021 14:09:37 +0200
Subject: [PATCH] add twp_frame_wand

---
 iris/program_logic/total_weakestpre.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 6278dc971..f2fd5b3e1 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -257,6 +257,12 @@ Proof. iIntros "[H Hwp]". iApply (twp_wand with "Hwp H"). Qed.
 Lemma twp_wand_r s E e Φ Ψ :
   WP e @ s; E [{ Φ }] ∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
 Proof. iIntros "[Hwp H]". iApply (twp_wand with "Hwp H"). Qed.
+Lemma twp_frame_wand s E e Φ R :
+  R -∗ WP e @ s; E [{ v, R -∗ Φ v }] -∗ WP e @ s; E [{ Φ }].
+Proof.
+  iIntros "HR HWP". iApply (twp_wand with "HWP").
+  iIntros (v) "HΦ". by iApply "HΦ".
+Qed.
 
 Lemma twp_wp_step s E e P Φ :
   TCEq (to_val e) None →
-- 
GitLab