val get8_def : s: FStar.Seq.Properties.lseq FStar.UInt8.t 1 -> FStar.UInt8.t
let get8_def (s:Seq.lseq U8.t 1) = Seq.index s 0
module Vale.Interop.Views

module DV = LowStar.BufferView.Down
module BV = LowStar.BufferView.Up
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Def.Opaque_s
open Vale.Lib.Seqs_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Seq
open Vale.Def.Words.Four_s

module U8 = FStar.UInt8
/
Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Seq.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Interop.Views.fsti
s: FStar.Seq.Properties.lseq FStar.UInt8.t 1 -> FStar.UInt8.t
FStar.Seq.Properties.lseq FStar.UInt8.t FStar.Seq.Base.index
let get8_def (s: Seq.lseq U8.t 1) =
  
Seq.index s 0