val lower_key (k: i_key)
  : GTot (k': s_key { lift_key k' = k })
val lower_key (k: i_key)
  : GTot (k': s_key { lift_key k' = k })
let lower_key (k: i_key)
  = let open T in
    let open GK in
    match k with
    | IntK k -> 
      KU.lower_merkle_key k;
      lift_lower_inv k;
      InternalKey (lower_base_key k)
    | AppK k -> ApplicationKey k
module Zeta.Steel.Rel

module GK = Zeta.GenKey
module T = Zeta.Steel.FormatsManual
module KU = Zeta.Steel.KeyUtils

let lift_key (k: s_key)
  : GTot i_key
  = let open T in
    let open GK in
    match k with
    | InternalKey k -> 
      KU.lift_internal_key k;
      IntK (lift_base_key k)
    | ApplicationKey k -> AppK k
/
Zeta.Time.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.BitUtils.fsti.checked Zeta.Record.fsti.checked Zeta.Hash.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.Rel.fst
k: Zeta.Steel.Rel.i_key -> Prims.GTot (k': Zeta.Steel.Rel.s_key{Zeta.Steel.Rel.lift_key k' = k})
Zeta.Steel.Rel.i_key Zeta.Key.merkle_key Zeta.Steel.LogEntry.Types.InternalKey Zeta.Steel.KeyUtils.lower_base_key Prims.unit Zeta.Steel.KeyUtils.lift_lower_inv Zeta.Steel.KeyUtils.lower_merkle_key Zeta.App.app_key Zeta.App.__proj__Mkapp_params__item__adm Zeta.Steel.Rel.app Zeta.Steel.LogEntry.Types.ApplicationKey Zeta.Steel.Rel.s_key Prims.b2t Prims.op_Equality Zeta.Steel.Rel.lift_key
let lower_key (k: i_key) =
  
let open T in
let open GK in
match k with
| IntK k ->
  KU.lower_merkle_key k;
  lift_lower_inv k;
  InternalKey (lower_base_key k)
| AppK k -> ApplicationKey k