diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index d3c948d43076cd86f3a44a9fd111b67919a3dcd5..8d98a5ee0bb2549dc5a9fd8bb7999c4c06db18bb 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -67,7 +67,7 @@ Section LiftingTests.
     wp_rec. wp_bin_op. wp_rec. wp_bin_op=> ?; wp_if.
     - rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
       by rewrite left_id impl_elim_l.
-    - assert (n1 = n2 - 1) as -> by omega; auto with I.
+    - wp_value. assert (n1 = n2 - 1) as -> by omega; auto with I.
   Qed.
 
   Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 164bb9b487061e111e0b27b2cf8d2186446c50b6..1ec6d231aa5ca96186f9583f6d78eb185c7fcd9f 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -16,7 +16,11 @@ Ltac wp_finish :=
   match goal with
   | |- ∀ _, _ => let H := fresh in intro H; go; revert H
   | |- _ ⊑ ▷ _ => etransitivity; [|apply later_mono; go; reflexivity]
-  | |- _ ⊑ wp _ _ _ => etransitivity; [|eapply wp_value; reflexivity]; simpl
+  | |- _ ⊑ wp _ _ _ =>
+     etransitivity; [|eapply wp_value; reflexivity];
+     (* sometimes, we will have to do a final view shift, so only apply
+     wp_value if we obtain a consecutive wp *)
+     match goal with |- _ ⊑ wp _ _ _ => simpl | _ => fail end
   | _ => idtac
   end in simpl; go.
 
@@ -55,7 +59,6 @@ Tactic Notation "wp_un_op" ">" :=
   end.
 Tactic Notation "wp_un_op" := wp_un_op>; wp_strip_later.
 Tactic Notation "wp_if" ">" :=
-  try wp_value;
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval cbv in e' with