From 824257bc3c2f553a70df533e32a3aefbd0911ddc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Feb 2016 20:49:06 +0100
Subject: [PATCH] Anti symmetry for sets.

---
 prelude/collections.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prelude/collections.v b/prelude/collections.v
index afe28a10c..e973f481a 100644
--- a/prelude/collections.v
+++ b/prelude/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.
-- 
GitLab