diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index cfdd88652e84cdbcf4edfd1f08041d58f0fd64da..26ddb58af2a2ae3f1e2989334c32d39ecfaa34c8 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -12,6 +12,18 @@ Ltac wp_simpl :=
       let e' := eval simpl in e in change (envs_entails Δ (wp E e' Q))
   end.
 
+Lemma tac_wp_simpl_subst `{heapG Σ} Δ E Φ e e' :
+  e = e' →
+  envs_entails Δ (WP e' @ E {{ Φ }}) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. by intros ->. Qed.
+
+Ltac wp_simpl_subst :=
+  try iStartProof;
+  try lazymatch goal with
+  | |- envs_entails ?Δ (wp ?E ?e ?Q) =>
+      eapply tac_wp_simpl_subst; [simpl_subst; reflexivity|]
+  end.
+
 Lemma tac_wp_pure `{heapG Σ} Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
@@ -41,7 +53,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       [apply _                        (* PureExec *)
       |try fast_done                  (* The pure condition for PureExec *)
       |apply _                        (* IntoLaters *)
-      |simpl_subst; try wp_value_head (* new goal *)
+      |wp_simpl_subst; try wp_value_head (* new goal *)
       ])
    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
   | _ => fail "wp_pure: not a 'wp'"
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index 28f75f6c8a26e77a3c6ceea613114910dac6c48e..01441c800708b8ba694685b2b7bfc5ddf8646215 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -40,7 +40,7 @@ Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
   {{{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }}}.
 Proof.
   iIntros (Φ) "[Hl Ht] HΦ".
-  iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); wp_rec; wp_let.
+  iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
   - iDestruct "Ht" as "%"; subst.
     wp_match. wp_load. wp_op. wp_store.
     by iApply ("HΦ" with "[$Hl]").