From 26dc475bb745f536649f71a68ba2bcd702d7275e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Apr 2020 00:45:43 +0200
Subject: [PATCH] Add lemma `subst_map_singleton`.
---
theories/heap_lang/metatheory.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 532eff0f2..ea41ee2d4 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).
--
GitLab