diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 11795f1fe02544d7c6db6d815182830a5f552c05..00d92652c508146332b832ea9a0e30a97ff035fd 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -71,7 +71,10 @@ Lemma wp_lam E xl e e' el Φ :
   Closed (xl +b+ []) e →
   subst_l xl el e = Some e' →
   ▷ WP e' @ E {{ Φ }} -∗ WP App (Lam xl e) el @ E {{ Φ }}.
-Proof. iIntros (???) "?". by iApply (wp_rec _ _ BAnon). Qed.
+Proof.
+  iIntros (???) "?". iApply (wp_rec _ _ BAnon)=>//.
+    by rewrite /= option_fmap_id.
+Qed.
 
 Lemma wp_let E x e1 e2 v Φ :
   to_val e1 = Some v →