diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 232867fb450ecd488b09832bde4a4cb42bbdfed1..ccbc2e5c212fd04b2e153874fa4aeda1fa0609a4 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -60,7 +60,7 @@ Implicit Types e : expr Λ.
 
 (* Weakest pre *)
 Lemma wp_unfold s E e Φ :
-  WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp (PROP:=iProp Σ)  s) E e Φ.
+  WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp (PROP:=iProp Σ) s) E e Φ.
 Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
 
 Global Instance wp_ne s E e n :