val related_key_inj_1 (sk: s_base_key) (ik0 ik1: i_base_key)
    : Lemma (requires related_base_key sk ik0 /\ related_base_key sk ik1)
      (ensures ik0 == ik1)
      [SMTPat (related_base_key sk ik0); SMTPat (related_base_key sk ik1)]
val related_key_inj_1 (sk: s_base_key) (ik0 ik1: i_base_key)
    : Lemma (requires related_base_key sk ik0 /\ related_base_key sk ik1)
      (ensures ik0 == ik1)
      [SMTPat (related_base_key sk ik0); SMTPat (related_base_key sk ik1)]
let related_key_inj_1 (sk:s_base_key) (ik0 ik1:i_base_key)
  : Lemma 
    (requires
      related_base_key sk ik0 /\
      related_base_key sk ik1)
    (ensures
      ik0 == ik1)
    [SMTPat (related_base_key sk ik0);
     SMTPat (related_base_key sk ik1)]
  = KeyUtils.lift_lower_inv ik0;
    KeyUtils.lift_lower_inv ik1
module Zeta.Steel.ThreadSim

open FStar.Classical

module M = Zeta.Merkle
module R = Zeta.Record
module KU = Zeta.Steel.KeyUtils
module TSM = Zeta.Steel.ThreadStateModel
module GK = Zeta.GenKey
module IS = Zeta.Intermediate.Store
module U32 = FStar.UInt32
/
Zeta.TimeKey.fsti.checked Zeta.Time.fsti.checked Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.RelHashFunction.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.IV.fst.checked Zeta.Record.fsti.checked Zeta.Merkle.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.HashFunction.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Steel.ThreadSim.fst
sk: Zeta.Steel.Rel.s_base_key -> ik0: Zeta.Steel.Rel.i_base_key -> ik1: Zeta.Steel.Rel.i_base_key
  -> FStar.Pervasives.Lemma
      (requires Zeta.Steel.Rel.related_base_key sk ik0 /\ Zeta.Steel.Rel.related_base_key sk ik1)
      (ensures ik0 == ik1)
      [
        SMTPat (Zeta.Steel.Rel.related_base_key sk ik0);
        SMTPat (Zeta.Steel.Rel.related_base_key sk ik1)
      ]
Zeta.Steel.Rel.s_base_key Zeta.Steel.Rel.i_base_key Zeta.Steel.KeyUtils.lift_lower_inv Prims.unit Prims.l_and Zeta.Steel.Rel.related_base_key Prims.squash Prims.eq2 Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.logical Prims.Nil
let related_key_inj_1 (sk: s_base_key) (ik0 ik1: i_base_key)
    : Lemma (requires related_base_key sk ik0 /\ related_base_key sk ik1)
      (ensures ik0 == ik1)
      [SMTPat (related_base_key sk ik0); SMTPat (related_base_key sk ik1)] =
  
KeyUtils.lift_lower_inv ik0;
KeyUtils.lift_lower_inv ik1