diff --git a/theories/collections.v b/theories/collections.v
index f3ed2dd95d42d6e1a6c0db253dc7e4d2d804b1d9..5e0a304b6c79edd66f5cdaa85d1ea65de5367149 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -24,6 +24,8 @@ Section simple_collection.
   Proof. firstorder auto. Qed.
   Global Instance: JoinSemiLattice C.
   Proof. firstorder auto. Qed.
+  Global Instance: AntiSymm (≡) (@collection_subseteq A C _).
+  Proof. done. Qed.
   Lemma elem_of_subseteq X Y : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y.
   Proof. done. Qed.
   Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.