diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 360b44585ac08e5ad082818e6561f2d518c01fa5..d36dd8d50a77da25e92996f4eca75d9228eef8f8 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -29,7 +29,9 @@ Tactic Notation "wp_rec" ">" :=
     | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
       match eval cbv in e' with
       | App (Rec _ _ _) _ =>
-         wp_bind K; etrans; [|eapply wp_rec; reflexivity]; wp_finish
+         wp_bind K; etrans;
+           [|eapply wp_rec; repeat (reflexivity || rewrite /= to_of_val)];
+           wp_finish
       end)
      end).
 Tactic Notation "wp_rec" := wp_rec>; try strip_later.
@@ -39,7 +41,9 @@ Tactic Notation "wp_lam" ">" :=
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval cbv in e' with
     | App (Rec "" _ _) _ =>
-       wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
+       wp_bind K; etrans;
+         [|eapply wp_lam; repeat (reflexivity || rewrite /= to_of_val)];
+         wp_finish
     end)
   end.
 Tactic Notation "wp_lam" := wp_lam>; try strip_later.