From 396540797c8070e579886f344a2d29a7d3e30f88 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 11:21:12 +0100
Subject: [PATCH] provide a way to get bbelow mkSet

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

diff --git a/theories/sets.v b/theories/sets.v
index f2b215a8..70c9610d 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -18,6 +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.
+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),
   mkSet (λ b, ∃ a, b ∈ f a ∧ a ∈ X).
-- 
GitLab