let nonempty_set (t: eqtype) =
  (s: Set.set t { exists x . set_def s x == true })
let nonempty_set (t: eqtype) =
(s: Set.set t {exists x. set_def s x == true})
Steel.ST.C.Types.UserStruct.fsti.checked
Steel.ST.Util.fsti.checked Steel.ST.C.Types.Struct.Aux.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Steel.ST.C.Types.UserStruct.fsti
Prims.eqtype FStar.Set.set Prims.l_Exists Prims.eq2 Prims.bool Steel.ST.C.Types.UserStruct.set_def
module Steel.ST.C.Types.UserStruct
open Steel.ST.Util
open Steel.ST.C.Types.Struct.Aux

module Set = FStar.Set

(* This library allows the user to define their own struct type, with
a constructor from field values, and a destructor to field values for
each field. This may be necessary for recursive structs *)

let set_def
  (#t: eqtype)
  (s: FStar.Set.set t)
  (x: t)
: Tot bool
= FStar.Set.mem x s

noextract
val nonempty_set : t: Prims.eqtype -> Type0
t: Prims.eqtype -> Type0