From ff44fd43a13760dd62f77b11be520f6669f4e6ea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Oct 2020 20:32:45 +0100
Subject: [PATCH] Oops.

---
 theories/fin_map_dom.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index cff6fd42..486ce529 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -90,6 +90,7 @@ Proof.
   destruct (decide (i = j)); set_solver.
 Qed.
 Lemma dom_insert_lookup {A} (m : M A) i x :
+  is_Some (m !! i) → dom D (<[i:=x]>m) ≡ dom D m.
 Proof. intros Hindom%elem_of_dom. rewrite dom_insert. set_solver. Qed.
 Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
 Proof. rewrite (dom_insert _). set_solver. Qed.
-- 
GitLab