val index_ (logs: all_logs) (t: tid) : tlog
val index_ (logs: all_logs) (t: tid) : tlog
let index_ (logs: all_logs)  (t: tid)
  : tlog
  = let tv = U16.v t in
    (t, Seq.index logs tv)
module Zeta.Steel.GlobalRel

open Zeta.App
open Zeta.AppSimulate
open Zeta.Steel.ApplicationTypes
open Zeta.Steel.ThreadStateModel
open Zeta.Steel.MultiSetHash
open Zeta.Steel.Rel
open Zeta.Steel.ThreadRel
open Zeta.Steel.Thread

module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module GG = Zeta.Generic.Global
module HA = Zeta.Steel.HashAccumulator
module StT = Zeta.Steel.Thread
module AH = Zeta.Steel.AggregateEpochHashes
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadRel.fsti.checked Zeta.Steel.Thread.fsti.checked Zeta.Steel.Rel.fsti.checked Zeta.Steel.MultiSetHash.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Steel.AggregateEpochHashes.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Intermediate.Global.fsti.checked Zeta.Generic.Global.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.GlobalRel.fsti
logs: Zeta.Steel.ThreadStateModel.all_logs -> t: Zeta.Steel.ApplicationTypes.tid
  -> Zeta.Steel.Thread.tlog
Zeta.Steel.ThreadStateModel.all_logs Zeta.Steel.ApplicationTypes.tid FStar.Pervasives.Native.Mktuple2 Zeta.Steel.ThreadStateModel.log FStar.Seq.Base.index FStar.UInt.uint_t FStar.UInt16.v Zeta.Steel.Thread.tlog
let index_ (logs: all_logs) (t: tid) : tlog =
  
let tv = U16.v t in
(t, Seq.index logs tv)