diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 66046172243eae95c625cbc43664635c5c1af58a..56cf8e923816008091472e68c60cb201eec9996f 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -95,4 +95,13 @@ Section heap.
   { eexists. eauto. }
   Qed.
 
+  Lemma wp_load E γ l v P Q :
+    nclose N ⊆ E →
+    P ⊑ heap_ctx γ →
+    P ⊑ (heap_mapsto γ l v ★ ▷ (heap_mapsto γ l v -★ Q v)) →
+    P ⊑ wp E (Load (Loc l)) Q.
+  Proof.
+    intros HN. rewrite /heap_mapsto. apply wp_load_heap; first done.
+    by simplify_map_equality.
+  Qed.
 End heap.