From e767481f734f0346f567cdc7e1fbae4e6ecbc533 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 11:48:18 +0100
Subject: [PATCH] sts: for disjointness, it is enough to demand being a subset
 of the empty set

---
 theories/sets.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/sets.v b/theories/sets.v
index f5e98f1c..0402ebc7 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -18,9 +18,9 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
 Instance set_collection : Collection A (set A).
 Proof. by split; [split | |]; repeat intro. Qed.
 
-Lemma mkSet_elem_of {A} (f : A → Prop) x : f x → x ∈ mkSet f.
+Lemma mkSet_elem_of {A} (f : A → Prop) x : (x ∈ mkSet f) = f x.
 Proof. done. Qed.
-Lemma mkSet_not_elem_of {A} (f : A → Prop) x : ~f x → x ∉ mkSet f.
+Lemma mkSet_not_elem_of {A} (f : A → Prop) x : (x ∉ mkSet f) = (~f x).
 Proof. done. Qed.
 
 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
-- 
GitLab