val nkey : n: Prims.nat -> Type0
let nkey (n:nat) = k:base_key{Zeta.BinTree.depth k = n}
module Zeta.MultiSetHashDomain

module K = Zeta.Key
module R = Zeta.Record
module M = Zeta.Merkle
/
Zeta.Record.fsti.checked Zeta.Merkle.fsti.checked Zeta.Key.fsti.checked Zeta.Hash.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.MultiSetHashDomain.fst
n: Prims.nat -> Type0
Prims.nat Zeta.Key.base_key Prims.b2t Prims.op_Equality Zeta.BinTree.depth
let nkey (n: nat) =
  
k: base_key{Zeta.BinTree.depth k = n}