diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index b932ce74f5cf6cf45ce1e810b3c049ecc6ec7037..ecca3cff5f55b3ee3f2b05612de492be4c852541 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -350,6 +350,7 @@ Section map.
   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.
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.