From c487567251cb78165e619084f0ae26e50fa76329 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Jan 2021 19:02:07 +0100
Subject: [PATCH] simplify proof (by Robbert)

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 82ca2fda..8a992203 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -881,12 +881,8 @@ Qed.
 Lemma map_to_list_delete {A} (m : M A) i x :
   m !! i = Some x → (i,x) :: map_to_list (delete i m) ≡ₚ map_to_list m.
 Proof.
-  intros Hmi. apply list_to_map_inj; csimpl.
-  - constructor; [|by auto using NoDup_fst_map_to_list].
-    rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
-    rewrite elem_of_map_to_list, lookup_delete in Hlookup. congruence.
-  - apply NoDup_fst_map_to_list.
-  - rewrite !list_to_map_to_list. rewrite insert_delete, insert_id; done.
+  intros. rewrite <-map_to_list_insert by (by rewrite lookup_delete).
+  by rewrite insert_delete, insert_id.
 Qed.
 
 Lemma map_to_list_submseteq {A} (m1 m2 : M A) :
-- 
GitLab