diff --git a/algebra/upred.v b/algebra/upred.v
index 9bb48f67ced62ac4d82da8261fd4fa8e205eb3a7..06b9b69d02ab138f97a276a4d5b7ff0339a0cc06 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -623,6 +623,21 @@ Lemma wand_elim_l' P Q R : P ⊑ (Q -★ R) → (P ★ Q) ⊑ R.
 Proof. intros ->; apply wand_elim_l. Qed.
 Lemma wand_elim_r' P Q R : Q ⊑ (P -★ R) → (P ★ Q) ⊑ R.
 Proof. intros ->; apply wand_elim_r. Qed.
+Lemma wand_apply_l P Q Q' R R' : P ⊑ (Q' -★ R') → R' ⊑ R → Q ⊑ Q' → (P ★ Q) ⊑ R.
+Proof. intros -> -> <-; apply wand_elim_l. Qed.
+Lemma wand_apply_r P Q Q' R R' : P ⊑ (Q' -★ R') → R' ⊑ R → Q ⊑ Q' → (Q ★ P) ⊑ R.
+Proof. intros -> -> <-; apply wand_elim_r. Qed.
+Lemma wand_apply_l' P Q Q' R : P ⊑ (Q' -★ R) → Q ⊑ Q' → (P ★ Q) ⊑ R.
+Proof. intros -> <-; apply wand_elim_l. Qed.
+Lemma wand_apply_r' P Q Q' R : P ⊑ (Q' -★ R) → Q ⊑ Q' → (Q ★ P) ⊑ R.
+Proof. intros -> <-; apply wand_elim_r. Qed.
+Lemma wand_frame_l P Q R : (Q -★ R) ⊑ (P ★ Q -★ P ★ R).
+Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
+Lemma wand_frame_r P Q R : (Q -★ R) ⊑ (Q ★ P -★ R ★ P).
+Proof.
+  apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc.
+  apply sep_mono_r, wand_elim_r.
+Qed.
 Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q).
 Proof. auto. Qed.
 Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q).
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 65e54aeca55e587939c1775b9f74bbae232fa902..f16ac33e6ed82c850e886c44427d7ffed179e5be 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -116,9 +116,9 @@ Section auth.
     rewrite (auth_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
     apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]comm.
-    (* Getting this wand eliminated is really annoying. *)
-    rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
-    rewrite wand_elim_r fsa_frame_l.
+    eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
+    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc. done. }
+    rewrite fsa_frame_l.
     apply (fsa_mono_pvs fsa)=> x.
     rewrite sep_exist_l; apply exist_elim=> L.
     rewrite sep_exist_l; apply exist_elim=> Lv.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index f8e47774586b5aa360568b6ab8387864ab040314..ea318637049004461efd2ad5c6328513e00fc883 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -133,9 +133,9 @@ Section sts.
     rewrite (sts_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
     apply (fsa_strip_pvs fsa). apply exist_elim=>s.
     rewrite (forall_elim s). rewrite [(▷_ ★ _)%I]comm.
-    (* Getting this wand eliminated is really annoying. *)
-    rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
-    rewrite wand_elim_r fsa_frame_l.
+    eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
+    { rewrite assoc [(_ ★ own _ _)%I]comm -assoc. done. }
+    rewrite fsa_frame_l.
     apply (fsa_mono_pvs fsa)=> x.
     rewrite sep_exist_l; apply exist_elim=> s'.
     rewrite sep_exist_l; apply exist_elim=>T'.