diff --git a/algebra/upred.v b/algebra/upred.v
index 00b7acba34a840914453aaf796f0321559b8a4eb..246bd71193addebb89e0b60d2775d464f6743bab 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -239,6 +239,10 @@ Proof.
   split; [|by intros [??]; apply (anti_symm (⊑))].
   intros HPQ; split; intros x i; apply HPQ.
 Qed.
+Lemma equiv_entails P Q : P ≡ Q → P ⊑ Q.
+Proof. apply equiv_spec. Qed.
+Lemma equiv_entails_sym P Q : Q ≡ P → P ⊑ Q.
+Proof. apply equiv_spec. Qed.
 Global Instance entails_proper :
   Proper ((≡) ==> (≡) ==> iff) ((⊑) : relation (uPred M)).
 Proof.
diff --git a/barrier/barrier.v b/barrier/barrier.v
index 2b1c3de334b34a051389e8e7f055a1bbca29026a..00c09830663ccfa877a6d72a7cf6bb4f5a3d66b0 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -255,6 +255,7 @@ Section proof.
       rewrite left_id -[(â–· barrier_inv _ _ _)%I]later_intro {3}/barrier_inv.
       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 -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i).
       rewrite !assoc.
@@ -264,7 +265,7 @@ Section proof.
       apply sts_ownS_weaken; eauto using sts.up_subseteq. }
     (* a High state: the comparison succeeds, and we perform a transition and
        return to the client *)
-    rewrite [(_ ★ (_ -★ _ ))%I]sep_elim_l.
+    rewrite [(_ ★ □ (_ → _ ))%I]sep_elim_l.
     rewrite -(exist_intro (State High (I ∖ {[ i ]}))) -(exist_intro ∅).
     change (i ∈ I) in Hs.
     rewrite const_equiv /=; last first.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 59b87e43ae3797a822abdc325f58c8d5e9cc9cfa..48753a97c0d69ac8bf97e243946f657d1326cb84 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -55,7 +55,7 @@ Section LiftingTests.
     revert n1. wp_rec=>n1 Hn.
     wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
     - rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
-      by rewrite left_id wand_elim_r.
+      by rewrite left_id -always_wand_impl always_elim wand_elim_r.
     - assert (n1 = n2 - 1) as -> by omega; auto with I.
   Qed.
 
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 93645fda38f1dd26620af31c8c633a134eb312f5..c461fd748c5bc831a78ea12f452b26afd6a5ccbf 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -16,13 +16,13 @@ Ltac u_strip_later :=
   let rec strip :=
       lazymatch goal with
       | |- (_ ★ _) ⊑ ▷ _  =>
-        etrans; last (eapply equiv_spec, later_sep);
+        etrans; last (eapply equiv_entails_sym, later_sep);
         apply sep_mono; strip
       | |- (_ ∧ _) ⊑ ▷ _  =>
-        etrans; last (eapply equiv_spec, later_and);
+        etrans; last (eapply equiv_entails_sym, later_and);
         apply sep_mono; strip
       | |- (_ ∨ _) ⊑ ▷ _  =>
-        etrans; last (eapply equiv_spec, later_or);
+        etrans; last (eapply equiv_entails_sym, later_or);
         apply sep_mono; strip
       | |- ▷ _ ⊑ ▷ _ => apply later_mono; reflexivity
       | |- _ ⊑ ▷ _ => apply later_intro; reflexivity
@@ -32,14 +32,14 @@ Ltac u_strip_later :=
     | |- _ ⊑ (_ ★ _) =>
       (* Force the later on the LHS to be top-level, matching laters
          below ★ on the RHS *)
-      etrans; first (apply equiv_spec; symmetry; apply later_sep; reflexivity);
+      etrans; first (apply equiv_entails, later_sep; reflexivity);
       (* Match the arm recursively *)
       apply sep_mono; shape_Q
     | |- _ ⊑ (_ ∧ _) =>
-      etrans; first (apply equiv_spec; symmetry; apply later_and; reflexivity);
+      etrans; first (apply equiv_entails, later_and; reflexivity);
       apply sep_mono; shape_Q
     | |- _ ⊑ (_ ∨ _) =>
-      etrans; first (apply equiv_spec; symmetry; apply later_or; reflexivity);
+      etrans; first (apply equiv_entails, later_or; reflexivity);
       apply sep_mono; shape_Q
     | |- _ ⊑ ▷ _ => apply later_mono; reflexivity
     (* We fail if we don't find laters in all branches. *)
@@ -48,32 +48,36 @@ Ltac u_strip_later :=
                          etrans; last eapply later_mono; first solve [ strip ]).
 
 (** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
-    into True ⊑ ∀..., ■?0... → ?1 -★ ?2, applies tac, and
+    into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and
     the moves all the assumptions back. *)
 Ltac u_revert_all :=
   lazymatch goal with
   | |- ∀ _, _ => let H := fresh in intro H; u_revert_all;
-             (* TODO: Really, we should distinguish based on whether this is a
-                dependent function type or not. Right now, we distinguish based
-                on the sort of the argument, which is suboptimal. *)
-             first [ apply (const_intro_impl _ _ _ H); clear H
-                   | revert H; apply forall_elim']
-  | |- ?C ⊑ _ => trans (True ★ C)%I;
-             first (rewrite [(True ★ C)%I]left_id; reflexivity);
-             apply wand_elim_l'
+           (* TODO: Really, we should distinguish based on whether this is a
+              dependent function type or not. Right now, we distinguish based
+              on the sort of the argument, which is suboptimal. *)
+           first [ apply (const_intro_impl _ _ _ H); clear H
+                 | revert H; apply forall_elim']
+  | |- ?C ⊑ _ => trans (True ∧ C)%I;
+           first (apply equiv_entails_sym, left_id, _; reflexivity);
+           apply impl_elim_l'
   end.
 
 (** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
    It applies löb where all the Coq assumptions have been turned into logical
    assumptions, then moves all the Coq assumptions back out to the context,
    applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the
-   Coq assumption so that we end up with the same shape as where we started. *)
+   Coq assumption so that we end up with the same shape as where we started,
+   but with an additional assumption ★-ed to the context *)
 Ltac u_löb tac :=
   u_revert_all;
+  (* Add a box *)
+  etrans; last (eapply always_elim; reflexivity);
   (* We now have a goal for the form True ⊑ P, with the "original" conclusion
      being locked. *)
   apply löb_strong; etransitivity;
-    first (apply equiv_spec; symmetry; apply (left_id _ _ _); reflexivity);
+    first (apply equiv_entails, left_id, _; reflexivity);
+  apply: always_intro;
   (* Now introduce again all the things that we reverted, and at the bottom,
      do the work *)
   let rec go :=
@@ -82,9 +86,12 @@ Ltac u_löb tac :=
                let H := fresh in intro H; go; revert H
       | |- _ ⊑ (■ _ → _) => apply impl_intro_l, const_elim_l;
                let H := fresh in intro H; go; revert H
-      (* This is the "bottom" of the goal, where we see the wand introduced
-         by u_revert_all as well as the ▷ from löb_strong. *)
-      | |- ▷ _ ⊑ (_ -★ _) => apply wand_intro_l; tac
+      (* This is the "bottom" of the goal, where we see the impl introduced
+         by u_revert_all as well as the ▷ from löb_strong and the □ we added. *)
+      | |- ▷ □ ?R ⊑ (?L → _) => apply impl_intro_l;
+               trans (L ★ ▷ □ R)%I;
+                 first (eapply equiv_entails, always_and_sep_r, _; reflexivity);
+               tac
       end
   in go.