diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 9f3180ba6384504292c3b69c9168ac424b6cac86..7f7ffb78bdcc076b8d9a6f484687a44094829de4 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -342,6 +342,25 @@ 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_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.
+  (** This cannot be using [=] because [list_to_set_singleton] does not hold for [=]. *)
+  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 *)
diff --git a/theories/list.v b/theories/list.v
index 7b91cdd80fa9b549bd9f709247a6cef2cbc570ea..71b761b15351f4f2fc7c8bf27d1264b14d60a55f 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3442,8 +3442,12 @@ Section fmap.
   Definition fmap_nil : f <$> [] = [] := eq_refl.
   Definition fmap_cons x l : f <$> x :: l = f x :: (f <$> l) := eq_refl.
 
+  Lemma list_fmap_singleton x : f <$> [x] = [f x].
+  Proof. reflexivity. Qed.
   Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
   Proof. by induction l1; f_equal/=. Qed.
+  Lemma fmap_snoc l x : f <$> l ++ [x] = (f <$> l) ++ [f x].
+  Proof. rewrite fmap_app, list_fmap_singleton. done. Qed.
   Lemma fmap_nil_inv k :  f <$> k = [] → k = [].
   Proof. by destruct k. Qed.
   Lemma fmap_cons_inv y l k :
diff --git a/theories/sets.v b/theories/sets.v
index 7b820ee7d1adb8f2b5421a9c0e9cea77416d0c72..7c144f92ca044384572be5f8890e961cdb7f4bd2 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -864,6 +864,10 @@ Section option_and_list_to_set.
   Proof. done. Qed.
   Lemma list_to_set_app l1 l2 : list_to_set (l1 ++ l2) ≡@{C} list_to_set l1 ∪ list_to_set l2.
   Proof. set_solver. Qed.
+  Lemma list_to_set_singleton x : list_to_set [x] ≡@{C} {[ x ]}.
+  Proof. set_solver. Qed.
+  Lemma list_to_set_snoc l x : list_to_set (l ++ [x]) ≡@{C} list_to_set l ∪ {[ x ]}.
+  Proof. set_solver. Qed.
   Global Instance list_to_set_perm : Proper ((≡ₚ) ==> (≡)) (list_to_set (C:=C)).
   Proof. induction 1; set_solver. Qed.