val lemma_lower_lift_key (k: s_key)
  : Lemma (ensures (lower_key (lift_key k) == k))
val lemma_lower_lift_key (k: s_key)
  : Lemma (ensures (lower_key (lift_key k) == k))
let lemma_lower_lift_key (k: s_key)
  : Lemma (ensures (lower_key (lift_key k) == k))
  = match k with
    | T.InternalKey k ->
      lower_lift_inv 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

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
/
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
  -> FStar.Pervasives.Lemma (ensures Zeta.Steel.Rel.lower_key (Zeta.Steel.Rel.lift_key k) == k)
Zeta.Steel.Rel.s_key Zeta.Steel.KeyUtils.internal_key Zeta.Steel.KeyUtils.lower_lift_inv Zeta.Steel.LogEntry.Types.key Prims.unit Prims.l_True Prims.squash Prims.eq2 Zeta.Steel.Rel.lower_key Zeta.Steel.Rel.lift_key Prims.Nil FStar.Pervasives.pattern
let lemma_lower_lift_key (k: s_key) : Lemma (ensures (lower_key (lift_key k) == k)) =
  
match k with
| T.InternalKey k -> lower_lift_inv k
| _ -> ()