diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 5da29d450190a2ea82399740b88dc2b74f97611c..3cc335765624ebfc9f5598ccb39d62b5ec3d1ae9 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -7,8 +7,8 @@ Definition assert : val :=
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 Global Opaque assert.
 
-Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) e `{!Closed [] e} :
-  WP e {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP assert: e {{ Φ }}.
+Lemma wp_assert {Σ} E (Φ : val → iProp heap_lang Σ) e `{!Closed [] e} :
+  WP e @ E {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP assert: e @ E {{ Φ }}.
 Proof.
   iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
   iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.