open Preamble

open Deqsets

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open Bool

open Relations

open Nat

open BitVector

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open BitVectorTrie

type bitVectorTrieSet = Types.unit0 BitVectorTrie.bitVectorTrie

val set_member :
  Nat.nat -> Bool.bool Vector.vector -> bitVectorTrieSet -> Bool.bool

val set_union :
  Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> bitVectorTrieSet

val set_eq : Nat.nat -> bitVectorTrieSet -> bitVectorTrieSet -> Bool.bool

val set_insert :
  Nat.nat -> BitVector.bitVector -> bitVectorTrieSet -> Types.unit0
  BitVectorTrie.bitVectorTrie

val set_empty : Nat.nat -> Types.unit0 BitVectorTrie.bitVectorTrie

val set_singleton :
  Nat.nat -> BitVector.bitVector -> Types.unit0 BitVectorTrie.bitVectorTrie