From 7e0096d81941e15e3e2d8d9ee63e969d599e7e32 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 18 Jan 2020 14:19:18 -0500
Subject: [PATCH] Add lemma `binder_delete_empty`.

---
 theories/binders.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/binders.v b/theories/binders.v
index ba5aca17..3fddac91 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -82,6 +82,9 @@ Section binder_delete_insert.
     Proper ((≡) ==> (≡) ==> (≡@{M A})) (binder_insert b).
   Proof. destruct b; solve_proper. Qed.
 
+  Lemma binder_delete_empty {A} b : binder_delete b ∅ =@{M A} ∅.
+  Proof. destruct b; simpl; auto using delete_empty. Qed.
+
   Lemma lookup_binder_delete_None {A} (m : M A) b s :
     binder_delete b m !! s = None ↔ b = BNamed s ∨ m !! s = None.
   Proof. destruct b; simpl; by rewrite ?lookup_delete_None; naive_solver. Qed.
-- 
GitLab