diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 189e50eb83f0552809b289743ad074481513a01b..5ccf36ab2d9dacba8c33606141c5eeb92b8a6d74 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -159,6 +159,9 @@ Proof. intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l. Qed.
 Lemma pvs_wand_r E1 E2 P Q R :
   P âŠ‘ (|={E1,E2}=> Q) â†’ (P â˜… (Q -â˜… R)) âŠ‘ (|={E1,E2}=> R).
 Proof. rewrite comm. apply pvs_wand_l. Qed.
+Lemma pvs_sep E P Q:
+  ((|={E}=> P) â˜… (|={E}=> Q)) âŠ‘ (|={E}=> P â˜… Q).
+Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
 
 Lemma pvs_mask_frame' E1 E1' E2 E2' P :
   E1' âŠ† E1 â†’ E2' âŠ† E2 â†’ E1 âˆ– E1' = E2 âˆ– E2' â†’