diff --git a/theories/gmap.v b/theories/gmap.v
index feff8ab1bade44e7b3fb62233bf5d8622b5b0ec1..4de585769b4401c1e22b2df1b72dc74724981915 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -237,11 +237,6 @@ Section gset.
   Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
   Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
-  Definition gset_to_propset (X : gset K) : propset K :=
-    {[ x | x ∈ X ]}.
-  Lemma elem_of_gset_to_propset (X : gset K) x : x ∈ gset_to_propset X ↔ x ∈ X.
-  Proof. done. Qed.
-
   Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
     (λ _, x) <$> mapset_car X.
 
diff --git a/theories/propset.v b/theories/propset.v
index 9d7165ad28b5db3dd226eb0fb927aad6fd894821..529dd471075eb1b5f217c1ebbcaa7c39ad729aca 100644
--- a/theories/propset.v
+++ b/theories/propset.v
@@ -34,6 +34,12 @@ Lemma top_subseteq {A} (X : propset A) : X ⊆ ⊤.
 Proof. done. Qed.
 Hint Resolve top_subseteq : core.
 
+Definition set_to_propset `{ElemOf A C} (X : C) : propset A :=
+  {[ x | x ∈ X ]}.
+Lemma elem_of_set_to_propset `{SemiSet A C} x (X : C) :
+  x ∈ set_to_propset X ↔ x ∈ X.
+Proof. done. Qed.
+
 Instance propset_ret : MRet propset := λ A (x : A), {[ x ]}.
 Instance propset_bind : MBind propset := λ A B (f : A → propset B) (X : propset A),
   PropSet (λ b, ∃ a, b ∈ f a ∧ a ∈ X).