diff --git a/theories/collections.v b/theories/collections.v
index 5e0a304b6c79edd66f5cdaa85d1ea65de5367149..93f3493d2988406e5085ec52ac6d9737d429123b 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -533,12 +533,21 @@ End fresh.
 Section collection_monad.
   Context `{CollectionMonad M}.
 
+  Global Instance collection_fmap_mono {A B} :
+    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B).
+  Proof. intros f g ? X Y ?; solve_elem_of. Qed.
   Global Instance collection_fmap_proper {A B} :
     Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
   Proof. intros f g ? X Y [??]; split; solve_elem_of. Qed.
+  Global Instance collection_bind_mono {A B} :
+    Proper (((=) ==> (⊆)) ==> (⊆) ==> (⊆)) (@mbind M _ A B).
+  Proof. unfold respectful; intros f g Hfg X Y ?; solve_elem_of. Qed.
   Global Instance collection_bind_proper {A B} :
     Proper (((=) ==> (≡)) ==> (≡) ==> (≡)) (@mbind M _ A B).
   Proof. unfold respectful; intros f g Hfg X Y [??]; split; solve_elem_of. Qed.
+  Global Instance collection_join_mono {A} :
+    Proper ((⊆) ==> (⊆)) (@mjoin M _ A).
+  Proof. intros X Y ?; solve_elem_of. Qed.
   Global Instance collection_join_proper {A} :
     Proper ((≡) ==> (≡)) (@mjoin M _ A).
   Proof. intros X Y [??]; split; solve_elem_of. Qed.
diff --git a/theories/sets.v b/theories/sets.v
index f2543ebeb5bda3ac1a01ac7d98056d59f09b1eae..f2b215a8ed9042e00c0d09709665e5c05c45a772 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -28,4 +28,4 @@ Instance set_join : MJoin set := λ A (XX : set (set A)),
 Instance set_collection_monad : CollectionMonad set.
 Proof. by split; try apply _. Qed.
 
-Global Opaque set_union set_intersection.
+Global Opaque set_union set_intersection set_difference.