From 4a5f19edf35d4c88c36b0471d37d3bb322f161db Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 4 Dec 2020 19:54:57 +0100
Subject: [PATCH] better proof by Robbert

---
 theories/fin_maps.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index bfbc2eeb..0453473c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -570,9 +570,7 @@ Qed.
 Lemma insert_subseteq_l {A} (m1 m2 : M A) i x :
   m2 !! i = Some x → m1 ⊆ m2 → <[i:=x]> m1 ⊆ m2.
 Proof.
-  intros Hi Hincl. replace m2 with (<[i:=x]> m2).
-  - apply insert_mono. done.
-  - apply insert_id. done.
+  intros Hi Hincl. etrans; [apply insert_mono, Hincl|]. by rewrite insert_id.
 Qed.
 
 Lemma insert_delete_subseteq {A} (m1 m2 : M A) i x :
-- 
GitLab