From 5a2cbf99deea7b0f56ef2a4a04722a062064d79f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Feb 2016 12:18:36 +0100
Subject: [PATCH] Conversion of gset to set.

---
 prelude/gmap.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/prelude/gmap.v b/prelude/gmap.v
index 88fa0ac29..77a83e6c2 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -3,7 +3,7 @@
 (** This file implements finite maps and finite sets with keys of any countable
 type. The implementation is based on [Pmap]s, radix-2 search trees. *)
 From prelude Require Export countable fin_maps fin_map_dom.
-From prelude Require Import pmap mapset.
+From prelude Require Import pmap mapset sets.
 
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
@@ -118,6 +118,10 @@ Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
 Instance gset_dom_spec `{Countable K} :
   FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
+Definition of_gset `{Countable A} (X : gset A) : set A := mkSet (λ x, x ∈ X).
+Lemma elem_of_of_gset `{Countable A} (X : gset A) x : x ∈ of_gset X ↔ x ∈ X.
+Proof. done. Qed.
+
 (** * Fresh elements *)
 (* This is pretty ad-hoc and just for the case of [gset positive]. We need a
 notion of countable non-finite types to generalize this. *)
-- 
GitLab