val stored_value : st: Zeta.High.Verifier.store_t app -> k: Zeta.Key.base_key{Zeta.High.Verifier.store_contains st k}
  -> Zeta.Record.value app
let stored_value (#app:_) = HV.stored_value #app
module Zeta.High.Merkle

module V = Zeta.GenericVerifier
module HV = Zeta.High.Verifier
module BP = Zeta.BinTreePtr
module M = Zeta.Merkle

open Zeta.Ghost
/
Zeta.Merkle.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.Hash.fsti.checked Zeta.Ghost.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.BinTreePtr.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
Zeta.High.Merkle.fst
st: Zeta.High.Verifier.store_t app -> k: Zeta.Key.base_key{Zeta.High.Verifier.store_contains st k}
  -> Zeta.Record.value app
Zeta.App.app_params Zeta.High.Verifier.stored_value Zeta.High.Verifier.store_t Zeta.Key.base_key Prims.b2t Zeta.High.Verifier.store_contains Zeta.Record.value
let stored_value (#app: _) =
  
HV.stored_value #app