val compare_nkey (n: nat) : cmp (nkey n)
val compare_nkey (n: nat) : cmp (nkey n)
let rec compare_nkey (n:nat)
  : cmp (nkey n)
  = let open Zeta.BinTree in
    let f =
        fun (k1 k2:nkey n) ->
          match k1, k2 with
          | Root, Root -> true
          | LeftChild _, RightChild _ -> true
          | RightChild _, LeftChild _ -> false
          | LeftChild c1, LeftChild c2
          | RightChild c1, RightChild c2  -> compare_nkey (n - 1) c1 c2
    in
    f
module Zeta.MultiSetHashDomain

module K = Zeta.Key
module R = Zeta.Record
module M = Zeta.Merkle

let nkey (n:nat) = k:base_key{Zeta.BinTree.depth k = n}
/
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 -> Zeta.MultiSet.cmp (Zeta.MultiSetHashDomain.nkey n)
Prims.nat Zeta.MultiSetHashDomain.nkey Prims.bool FStar.Pervasives.Native.Mktuple2 Zeta.BinTree.bin_tree_node Zeta.MultiSetHashDomain.compare_nkey Prims.op_Subtraction Zeta.MultiSet.cmp
let rec compare_nkey (n: nat) : cmp (nkey n) =
  
let open Zeta.BinTree in
let f =
  fun (k1: nkey n) (k2: nkey n) ->
    match k1, k2 with
    | Root, Root -> true
    | LeftChild _, RightChild _ -> true
    | RightChild _, LeftChild _ -> false
    | LeftChild c1, LeftChild c2 | RightChild c1, RightChild c2 -> compare_nkey (n - 1) c1 c2
in
f