diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 41d2b5e188f69c06cd57d90b66889336aa8d7b13..d27181d85024bc3b6c6708f8a7643e501da29405 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -146,6 +146,14 @@ Lemma pvs_impl_l E1 E2 P Q : (â–¡ (P â†’ Q) âˆ§ pvs E1 E2 P) âŠ‘ pvs E1 E2 Q.
 Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
 Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P âˆ§ â–¡ (P â†’ Q)) âŠ‘ pvs E1 E2 Q.
 Proof. by rewrite comm pvs_impl_l. Qed.
+Lemma pvs_wand_l E1 E2 P Q R :
+  P âŠ‘ pvs E1 E2 Q â†’ ((Q -â˜… R) â˜… P) âŠ‘ pvs E1 E2 R.
+Proof.
+  intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l.
+Qed.
+Lemma pvs_wand_r E1 E2 P Q R :
+  P âŠ‘ pvs E1 E2 Q â†’ (P â˜… (Q -â˜… R)) âŠ‘ pvs E1 E2 R.
+Proof. rewrite comm. apply pvs_wand_l. Qed.
 
 Lemma pvs_mask_frame' E1 E1' E2 E2' P :
   E1' âŠ† E1 â†’ E2' âŠ† E2 â†’ E1 âˆ– E1' = E2 âˆ– E2' â†’ pvs E1' E2' P âŠ‘ pvs E1 E2 P.