From 7d0a702775a6e82978cc50e7704566fedc20d9da Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 20 Apr 2021 10:25:16 +0200
Subject: [PATCH] Some proof cleanup

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b720debf..a30f41b0 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1380,8 +1380,8 @@ Section map_filter_misc.
   Lemma map_filter_empty' m :
     map_Forall (λ k v, ¬ P (k,v)) m → filter P m = ∅.
   Proof.
-    intros HA. apply map_eq. intros i'. rewrite lookup_empty.
-    apply map_filter_lookup_None. right. apply HA.
+    intros HA. apply map_empty. intros i'.
+    apply map_filter_lookup_None. right. by apply HA.
   Qed.
 
   Lemma map_filter_empty : filter P (∅ : M A) = ∅.
-- 
GitLab