diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 115ff663af930e4037fbd1b485368a028c428501..6343b8ee6f32e37157ab7d315525987fa62f4d7a 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -79,6 +79,12 @@ Section heap.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
   Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
 
+  Lemma heap_mapsto_valid l q v : l ↦{q} v ⊢ ✓ q.
+  Proof.
+    rewrite heap_mapsto_eq /heap_mapsto_def auth_own_valid !discrete_valid.
+    by apply pure_mono=> /singleton_valid [??].
+  Qed.
+
   Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
   Proof.
     by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.