From 847196740e44c2f4387cc88f464c34914b60eb57 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Feb 2017 16:42:27 +0100
Subject: [PATCH] Add a variant of lookup_insert_is_Some.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index fe9d0f36..2d10c3f8 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -425,6 +425,9 @@ Qed.
 Lemma lookup_insert_is_Some {A} (m : M A) i j x :
   is_Some (<[i:=x]>m !! j) ↔ i = j ∨ i ≠ j ∧ is_Some (m !! j).
 Proof. unfold is_Some; setoid_rewrite lookup_insert_Some; naive_solver. Qed.
+Lemma lookup_insert_is_Some' {A} (m : M A) i j x :
+  is_Some (<[i:=x]>m !! j) ↔ i = j ∨ is_Some (m !! j).
+Proof. rewrite lookup_insert_is_Some. destruct (decide (i=j)); naive_solver. Qed.
 Lemma lookup_insert_None {A} (m : M A) i j x :
   <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠ j.
 Proof.
-- 
GitLab