diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 532eff0f2d13d46b555985c1af84df4b6cc0f380..ea41ee2d4323db892a31217c0be9d5bc46cb8b10 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -183,6 +183,10 @@ Proof.
     + by rewrite /= binder_delete_insert // delete_insert_delete
         !binder_delete_delete delete_idemp.
 Qed.
+Lemma subst_map_singleton x v e :
+  subst_map {[x:=v]} e = subst x v e.
+Proof. by rewrite subst_map_insert delete_empty subst_map_empty. Qed.
+
 Lemma subst_map_binder_insert b v vs e :
   subst_map (binder_insert b v vs) e =
   subst' b v (subst_map (binder_delete b vs) e).