val lift_key (k: s_key)
  : GTot i_key
val lift_key (k: s_key)
  : GTot i_key
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
module Zeta.Steel.Rel

module GK = Zeta.GenKey
module T = Zeta.Steel.FormatsManual
module KU = Zeta.Steel.KeyUtils
/
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.s_key -> Prims.GTot Zeta.Steel.Rel.i_key
Zeta.Steel.Rel.s_key Zeta.Steel.KeyUtils.internal_key Zeta.GenKey.IntK Zeta.Steel.Rel.app Zeta.Steel.KeyUtils.lift_base_key Prims.unit Zeta.Steel.KeyUtils.lift_internal_key Zeta.Steel.ApplicationTypes.key_type Zeta.GenKey.AppK Zeta.Steel.Rel.i_key
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