diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index ee50b4a81d85c38947bf815dff736da89666f5af..7d45d55010816376fda543e59271b8d1ac3c1a8c 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -111,15 +111,11 @@ Proof.
   intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_rec_locked E f x erec (e1 e2 : expr) Φ `{!Closed (f :b: x :b: []) erec} :
+Lemma wp_rec_locked E f x erec e1 e2 Φ `{!Closed (f :b: x :b: []) erec} :
   e1 = of_val $ locked (RecV f x erec) →
   is_Some (to_val e2) →
   ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
-Proof.
-  intros -> [v2 ?]. unlock. rewrite -(wp_lift_pure_det_head_step' (App _ _)
-    (subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
-  intros; inv_head_step; eauto.
-Qed.
+Proof. unlock. auto using wp_rec. Qed.
 
 Lemma wp_un_op E op e v v' Φ :
   to_val e = Some v →