diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 6cb031f7430ba8da5a7dc0d5ee8b9d6098b1d4c9..1ecf5771d8b479674e55f9ad67124c9365ffbfc3 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -56,7 +56,8 @@ Ltac uLöb tac :=
                let H := fresh in intro H; go; revert H
       | |- ▷ ?R ⊑ (?L -★ locked _) => apply wand_intro_l;
                (* TODO: Do sth. more robust than rewriting. *)
-               trans (▷ (L ★ R))%I; first (rewrite later_sep -(later_intro L); reflexivity );
+               trans (▷ L ★ ▷ R)%I; first (apply sep_mono_l, later_intro; reflexivity);
+               trans (▷ (L ★ R))%I; first (apply equiv_spec, later_sep; reflexivity );
                unlock; tac
       end
   in go.