From e37b4e68989192943f3f4bfcba80dee3ec8ab1e5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jan 2021 11:20:34 +0100
Subject: [PATCH] add set_map_empty

---
 theories/fin_sets.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 2cb8a475..b932ce74 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -343,6 +343,10 @@ Section map.
     x ∈ X → y = f x → y ∈ set_map (D:=D) f X.
   Proof. set_solver. Qed.
 
+  Lemma set_map_empty (f : A → B) :
+    set_map (C:=C) (D:=D) f ∅ = ∅.
+  Proof. unfold set_map. rewrite elements_empty. done. Qed.
+
   Lemma set_map_union (f : A → B) (X Y : C) :
     set_map (D:=D) f (X ∪ Y) ≡ set_map (D:=D) f X ∪ set_map (D:=D) f Y.
   Proof. set_solver. Qed.
-- 
GitLab