diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 2b17a775055d61fba19e93811bf5cd4e17384709..1dcf85049b04cb0b13991192f73686427cc4f5bf 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -46,7 +46,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
-    [unlock; simpl; apply _   (* PureExec *)
+    [unlock; simpl; apply _                  (* PureExec *)
     |wp_pure_done             (* The pure condition for PureExec *)
     |apply _                  (* IntoLaters *)
     |simpl_subst; try wp_value_head (* new goal *)])
@@ -86,7 +86,7 @@ Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (iResUR Σ).
 
 Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
-  to_val e = Some v →
+  IntoVal e v →
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
@@ -111,7 +111,7 @@ Proof.
 Qed.
 
 Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
-  to_val e = Some v' →
+  IntoVal e v' →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
@@ -124,7 +124,7 @@ Proof.
 Qed.
 
 Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 v2 Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  IntoVal e1 v1 → IntoVal e2 v2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
   (Δ' ⊢ WP fill K (Lit (LitBool false)) @ E {{ Φ }}) →
@@ -136,7 +136,7 @@ Proof.
 Qed.
 
 Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ :
-  to_val e1 = Some v1 → to_val e2 = Some v2 →
+  IntoVal e1 v1 → IntoVal e2 v2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
@@ -166,11 +166,10 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ H K))
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-    [let e' := match goal with |- to_val ?e' = _ => e' end in
-     wp_done || fail "wp_alloc:" e' "not a value"
-    |apply _
+    [apply _
     |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
       eexists; split;
         [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
@@ -200,11 +199,10 @@ Tactic Notation "wp_store" :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ _ K))
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_wp_store _ _ _ _ _ K); [apply _|..])
       |fail 1 "wp_store: cannot find 'Store' in" e];
-    [let e' := match goal with |- to_val ?e' = _ => e' end in
-     wp_done || fail "wp_store:" e' "not a value"
-    |apply _
+    [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
      iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
     |env_cbv; reflexivity
@@ -217,13 +215,10 @@ Tactic Notation "wp_cas_fail" :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ K))
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
-    [let e' := match goal with |- to_val ?e' = _ => e' end in
-     wp_done || fail "wp_cas_fail:" e' "not a value"
-    |let e' := match goal with |- to_val ?e' = _ => e' end in
-     wp_done || fail "wp_cas_fail:" e' "not a value"
-    |apply _
+    [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
      iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
     |try congruence
@@ -236,13 +231,10 @@ Tactic Notation "wp_cas_suc" :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ K))
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
-    [let e' := match goal with |- to_val ?e' = _ => e' end in
-     wp_done || fail "wp_cas_suc:" e' "not a value"
-    |let e' := match goal with |- to_val ?e' = _ => e' end in
-     wp_done || fail "wp_cas_suc:" e' "not a value"
-    |apply _
+    [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
      iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
     |try congruence
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 8db1ef4e7b196cb8f32423969b4b359a3273726d..51681a36571459c2906a42b24794d8fbce80cfbf 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -42,6 +42,16 @@ Section LiftingTests.
     by repeat (wp_pure _).
   Qed.
 
+  Definition heap_e4 : expr :=
+    let: "x" := (let: "y" := ref (ref #1) in ref "y") in
+    ! ! !"x".
+
+  Lemma heap_e4_spec : WP heap_e4 {{ v, ⌜ v = #1 ⌝ }}%I.
+  Proof.
+    rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
+    wp_alloc l''. wp_let. by repeat wp_load.
+  Qed.
+
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
       let: "yp" := "y" + #1 in