val key_lt : n1: Zeta.BinTree.bin_tree_node -> n2: Zeta.BinTree.bin_tree_node -> Prims.bool
let key_lt = Zeta.BinTree.lt
module Zeta.GenericVerifier

open Zeta.Ghost
open Zeta.App
open Zeta.AppSimulate
open Zeta.Time
open Zeta.MultiSetHashDomain
open Zeta.Record

module S = FStar.Seq
module SA = Zeta.SeqAux
module MSD = Zeta.MultiSetHashDomain

(* identifier type for verifier threads *)
let thread_id = Zeta.Thread.thread_id
/
Zeta.TimeKey.fsti.checked Zeta.Time.fsti.checked Zeta.Thread.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.Key.fsti.checked Zeta.Ghost.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.GenericVerifier.fsti
n1: Zeta.BinTree.bin_tree_node -> n2: Zeta.BinTree.bin_tree_node -> Prims.bool
Zeta.BinTree.lt
let key_lt =
  
Zeta.BinTree.lt