From 41ad05c6fc675f93eb9aee81b8313dfb704a006c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Jul 2016 18:15:29 +0200
Subject: [PATCH] Frame under a wand.

---
 proofmode/classes.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/proofmode/classes.v b/proofmode/classes.v
index d2e0eefd3..b84436e8e 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -256,6 +256,13 @@ Global Instance frame_or R P1 P2 Q1 Q2 Q :
   Frame R P1 Q1 → Frame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
 Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
 
+Global Instance frame_wand R P1 P2 Q2 :
+  Frame R P2 Q2 → Frame R (P1 -★ P2) (P1 -★ Q2).
+Proof.
+  rewrite /Frame=> ?. apply wand_intro_l.
+  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
+Qed.
+
 Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP.
 Global Instance make_later_true : MakeLater True True.
 Proof. by rewrite /MakeLater later_True. Qed.
-- 
GitLab