val root:r: Zeta.BinTree.bin_tree_node{Zeta.BinTree.depth r = 0}
val root:r: Zeta.BinTree.bin_tree_node{Zeta.BinTree.depth r = 0}
let root : r:Zeta.BinTree.bin_tree_node { Zeta.BinTree.depth r = 0 } = Zeta.BinTree.Root
module Zeta.High.Interleave

open FStar.Classical

open Zeta.Ghost
/
Zeta.SeqIdx.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.Ghost.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.High.Interleave.fst
r: Zeta.BinTree.bin_tree_node{Zeta.BinTree.depth r = 0}
Zeta.BinTree.Root
let root:r: Zeta.BinTree.bin_tree_node{Zeta.BinTree.depth r = 0} =
  
Zeta.BinTree.Root