From 0b7821f17903ee5304e20d74fd734e8bba5d8662 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 11:27:27 +0100
Subject: [PATCH] we also need to go below mkSet for \notin

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

diff --git a/theories/sets.v b/theories/sets.v
index 70c9610d..f5e98f1c 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -20,6 +20,8 @@ Proof. by split; [split | |]; repeat intro. Qed.
 
 Lemma mkSet_elem_of {A} (f : A → Prop) x : f x → x ∈ mkSet f.
 Proof. done. Qed.
+Lemma mkSet_not_elem_of {A} (f : A → Prop) x : ~f x → x ∉ mkSet f.
+Proof. done. Qed.
 
 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
 Instance set_bind : MBind set := λ A B (f : A → set B) (X : set A),
-- 
GitLab