diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 29d6219e443a66a2f396b8608ceb8fb08faf0975..89f3f4bbb787109afd186e05b74f3b72f85f16cc 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -117,7 +117,7 @@ Proof.
   intros HN. rewrite /newbarrier. wp_seq.
   rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
   apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
-  rewrite !assoc. apply pvs_wand_r.
+  rewrite !assoc. rewrite- pvs_wand_r; apply sep_mono_l.
   (* The core of this proof: Allocating the STS and the saved prop. *)
   eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=idCF) _ P).
   rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
@@ -201,7 +201,7 @@ Proof.
     rewrite -!assoc. apply sep_mono_r, sep_mono_r, wand_intro_l.
     wp_op; first done. intros _. wp_if. rewrite !assoc.
     rewrite -always_wand_impl always_elim.
-    rewrite -{2}pvs_wp. apply pvs_wand_r.
+    rewrite -{2}pvs_wp. rewrite -pvs_wand_r; apply sep_mono_l.
     rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i).
     rewrite const_equiv // left_id -later_intro.
     ecancel_pvs [heap_ctx _; saved_prop_own _ _; Q -★ _; R -★ _; sts_ctx _ _ _]%I.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index ba3fb38c2644c1daf96e9e2af51e0addaf16db03..e723026188cdb460e52ac7a67ca5cee2af0835ae 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -159,12 +159,10 @@ Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ (|={E1,E2}=> P)) ⊢ (|={E1,E2}=
 Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
 Lemma pvs_impl_r E1 E2 P Q : ((|={E1,E2}=> P) ∧ □ (P → Q)) ⊢ (|={E1,E2}=> Q).
 Proof. by rewrite comm pvs_impl_l. Qed.
-Lemma pvs_wand_l E1 E2 P Q R :
-  P ⊢ (|={E1,E2}=> Q) → ((Q -★ R) ★ P) ⊢ (|={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 ⊢ (|={E1,E2}=> Q) → (P ★ (Q -★ R)) ⊢ (|={E1,E2}=> R).
-Proof. rewrite comm. apply pvs_wand_l. Qed.
+Lemma pvs_wand_l E1 E2 P Q : ((P -★ Q) ★ (|={E1,E2}=> P)) ⊢ (|={E1,E2}=> Q).
+Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
+Lemma pvs_wand_r E1 E2 P Q : ((|={E1,E2}=> P) ★ (P -★ Q)) ⊢ (|={E1,E2}=> Q).
+Proof. by rewrite pvs_frame_r wand_elim_r. 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.