diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 0072425495af4c754c8271540293c6c7ec2b9cfa..a793ec715a52a385be8c8dc8d6faf7566faa516e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -222,7 +222,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
   iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; iApply lem; try iNext)
+    wp_bind_core K; iApply lem; try iNext; simpl)
   | _ => fail "wp_apply: not a 'wp'"
   end.