diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 56bd2a2674af965d874457af220f6c99e14e5dfe..82275d0f3d9a0e3616de7feb92507027cdb72f97 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -16,6 +16,10 @@ Lemma wp_ectx_bind {E Φ} K e :
   WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
 Proof. apply: weakestpre.wp_bind. Qed.
 
+Lemma wp_ectx_bind_inv {E Φ} K e :
+  WP fill K e @ E {{ Φ }} ⊢ WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}.
+Proof. apply: weakestpre.wp_bind_inv. Qed.
+
 Lemma wp_lift_head_step {E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗