From 395695866f8ebf8bd1aaaaa7f225ff10b031a022 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 12 Nov 2018 01:00:38 +0100
Subject: [PATCH] Prove map_Forall_delete.

---
 theories/fin_maps.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 67b242f3..7185a59f 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1119,6 +1119,8 @@ Proof.
   naive_solver eauto using map_Forall_insert_11,
     map_Forall_insert_12, map_Forall_insert_2.
 Qed.
+Lemma map_Forall_delete m i : map_Forall P m → map_Forall P (delete i m).
+Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
 Lemma map_Forall_ind (Q : M A → Prop) :
   Q ∅ →
   (∀ m i x, m !! i = None → P i x → map_Forall P m → Q m → Q (<[i:=x]>m)) →
-- 
GitLab