diff --git a/CHANGELOG.md b/CHANGELOG.md
index c9d90f7fdb005bfc9738f1968eab312839012af0..0f37282c97dd935faf0035cdd17bb91542cf16ba 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -95,6 +95,8 @@ longer supported by this release.
 - Rename `fmap_inj` → `list_fmap_eq_inj` and `option_fmap_inj` →
   `option_fmap_eq_inj`. The new lemmas `list_fmap_inj`/`option_fmap_inj`
   generalize injectivity to `Forall2`/`option_Forall2`.
+- Generalize `set_map`, `set_bind`, `set_omap`, `map_to_set` and `map_img`
+  lemmas from `Set_` to `SemiSet`.
 
 **Changes in `stdpp_unstable`:**
 
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 596b3dbf4ef9e514b8eae42de65c7198a80ee029..83a349d37876e77f1a329e75d042b2423cc55de9 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1272,7 +1272,7 @@ Proof.
 Qed.
 
 Section map_to_set.
-  Context {A : Type} `{Set_ B C}.
+  Context {A : Type} `{SemiSet B C}.
 
   Lemma elem_of_map_to_set (f : K → A → B) (m : M A) (y : B) :
     y ∈ map_to_set (C:=C) f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y.
@@ -1297,7 +1297,7 @@ Section map_to_set.
   Proof. unfold_leibniz. apply map_to_set_insert. Qed.
 End map_to_set.
 
-Lemma elem_of_map_to_set_pair `{Set_ (K * A) C} (m : M A) i x :
+Lemma elem_of_map_to_set_pair `{SemiSet (K * A) C} (m : M A) i x :
   (i,x) ∈@{C} map_to_set pair m ↔ m !! i = Some x.
 Proof. rewrite elem_of_map_to_set. naive_solver. Qed.
 
@@ -3988,7 +3988,7 @@ End preimg.
 
 (** ** The [map_img] (image/codomain) operation *)
 Section img.
-  Context `{FinMap K M, Set_ A SA}.
+  Context `{FinMap K M, SemiSet A SA}.
   Implicit Types m : M A.
   Implicit Types x y : A.
   Implicit Types X : SA.
@@ -4197,26 +4197,26 @@ Section img.
   Proof. constructor. by rewrite map_img_singleton, elem_of_singleton. Qed.
 End img.
 
-Lemma map_img_fmap `{FinMap K M, FinSet A SA, Set_ B SB} (f : A → B) (m : M A) :
+Lemma map_img_fmap `{FinMap K M, FinSet A SA, SemiSet B SB} (f : A → B) (m : M A) :
   map_img (f <$> m) ≡@{SB} set_map (C:=SA) f (map_img m).
 Proof.
   apply set_equiv. intros y. rewrite elem_of_map_img, elem_of_map.
   setoid_rewrite lookup_fmap. setoid_rewrite fmap_Some.
   setoid_rewrite elem_of_map_img. naive_solver.
 Qed.
-Lemma map_img_fmap_L `{FinMap K M, FinSet A SA, Set_ B SB, !LeibnizEquiv SB}
+Lemma map_img_fmap_L `{FinMap K M, FinSet A SA, SemiSet B SB, !LeibnizEquiv SB}
     (f : A → B) (m : M A) :
   map_img (f <$> m) =@{SB} set_map (C:=SA) f (map_img m).
 Proof. unfold_leibniz. apply map_img_fmap. Qed.
 
-Lemma map_img_kmap `{FinMap K M, FinMap K2 M2, Set_ A SA}
+Lemma map_img_kmap `{FinMap K M, FinMap K2 M2, SemiSet A SA}
     (f : K → K2) `{!Inj (=) (=) f} m :
   map_img (kmap (M2:=M2) f m) ≡@{SA} map_img m.
 Proof.
   apply set_equiv. intros x. rewrite !elem_of_map_img.
   setoid_rewrite (lookup_kmap_Some f). naive_solver.
 Qed.
-Lemma map_img_kmap_L `{FinMap K M, FinMap K2 M2, Set_ A SA, !LeibnizEquiv SA}
+Lemma map_img_kmap_L `{FinMap K M, FinMap K2 M2, SemiSet A SA, !LeibnizEquiv SA}
     (f : K → K2) `{!Inj (=) (=) f} m :
   map_img (kmap (M2:=M2) f m) =@{SA} map_img m.
 Proof. unfold_leibniz. by apply map_img_kmap. Qed.
diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index d23891f338222f053552cbfb3c7bc81a1874054f..2e054d4211791367b3967798f77ea4d588ee78b1 100644
--- a/stdpp/fin_sets.v
+++ b/stdpp/fin_sets.v
@@ -422,7 +422,7 @@ End filter.
 
 (** * Map *)
 Section map.
-  Context `{Set_ B D}.
+  Context `{SemiSet B D}.
 
   Lemma elem_of_map (f : A → B) (X : C) y :
     y ∈ set_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X.
@@ -474,7 +474,7 @@ End map.
 
 (** * Bind *)
 Section set_bind.
-  Context `{Set_ B SB}.
+  Context `{SemiSet B SB}.
 
   Local Notation set_bind := (set_bind (A:=A) (SA:=C) (SB:=SB)).
 
@@ -521,7 +521,7 @@ End set_bind.
 
 (** * OMap *)
 Section set_omap.
-  Context `{Set_ B D}.
+  Context `{SemiSet B D}.
   Implicit Types (f : A → option B).
   Implicit Types (x : A) (y : B).
   Notation set_omap := (set_omap (C:=C) (D:=D)).