From bf59b1eb5726360b011c65165c2b79a564298278 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 12 Jan 2021 18:24:04 +0100
Subject: [PATCH] add set_map_union, set_map_singleton

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

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 9f3180ba..2cb8a475 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -342,6 +342,20 @@ Section map.
   Lemma elem_of_map_2_alt (f : A → B) (X : C) (x : A) (y : B) :
     x ∈ X → y = f x → y ∈ set_map (D:=D) f X.
   Proof. set_solver. 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.
+  Lemma set_map_singleton (f : A → B) (x : A) :
+    set_map (C:=C) (D:=D) f {[x]} ≡ {[f x]}.
+  Proof. set_solver. Qed.
+
+  Lemma set_map_union_L `{!LeibnizEquiv D} (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. unfold_leibniz. apply set_map_union. Qed.
+  Lemma set_map_singleton_L `{!LeibnizEquiv D} (f : A → B) (x : A) :
+    set_map (C:=C) (D:=D) f {[x]} = {[f x]}.
+  Proof. unfold_leibniz. apply set_map_singleton. Qed.
 End map.
 
 (** * Decision procedures *)
-- 
GitLab