From 1e1dbb1401dc412bb0cbedf455d9301488d1b4c2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 4 Sep 2021 22:41:51 -0400
Subject: [PATCH] use a different work-around

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e2d7f68c..8b0a6ea3 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2298,8 +2298,7 @@ Lemma map_size_disj_union {A} (m1 m2 : M A) :
   m1 ##ₘ m2 → size (m1 ∪ m2) = size m1 + size m2.
 Proof.
   intros Hdisj. induction m1 as [|k x m1 Hm1 IH] using map_ind.
-  { rewrite map_empty_union. (* FIXME: [rewrite left_id] leaves a goal *)
-    rewrite map_size_empty. done. }
+  { rewrite (left_id _ _), map_size_empty. done. }
   rewrite <-insert_union_l.
   rewrite map_size_insert.
   rewrite lookup_union_r by done.
-- 
GitLab