Anti symmetry for sets.

79421f72 · Robbert Krebbers · c2e4e322 · 79421f72
Commit 79421f72 authored Feb 15, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

theories/collections.v theories/collections.v +2 -0

No files found.
--- 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.