diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 137aa6adb9d9b68658b170adc4b033142067ea8e..973c1eb940af4ad284caa5a949b1ac8053cbcfe8 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -206,6 +206,8 @@ Lemma wp_strip_pvs E e P Q : P ⊑ wp E e Q → pvs E E P ⊑ wp E e Q.
 Proof. move=>->. by rewrite pvs_wp. Qed.
 Lemma wp_value E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
 Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
+Lemma wp_value_pvs E Q e v : to_val e = Some v → pvs E E (Q v) ⊑ wp E e Q.
+Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
 Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
 Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
 Lemma wp_frame_later_l E e Q R :