val parse_seq_flbytes_gen (sz: nat) (s: bytes{Seq.length s == sz}) : Tot (Seq.lseq byte sz)
let parse_seq_flbytes_gen
  (sz: nat)
  (s: bytes { Seq.length s == sz } )
: Tot (Seq.lseq byte sz)
= s
val parse_seq_flbytes_gen (sz: nat) (s: bytes{Seq.length s == sz}) : Tot (Seq.lseq byte sz)
let parse_seq_flbytes_gen (sz: nat) (s: bytes{Seq.length s == sz}) : Tot (Seq.lseq byte sz) =
s
LowParse.Spec.SeqBytes.Base.fst.checked
prims.fst.checked LowParse.Spec.FLData.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.SeqBytes.Base.fst
Prims.nat LowParse.Bytes.bytes Prims.eq2 FStar.Seq.Base.length LowParse.Bytes.byte FStar.Seq.Properties.lseq
module LowParse.Spec.SeqBytes.Base
include LowParse.Spec.FLData

let parse_seq_flbytes_gen
  (sz: nat)
  (s: bytes { Seq.length s == sz } )
val parse_seq_flbytes_gen (sz: nat) (s: bytes{Seq.length s == sz}) : Tot (Seq.lseq byte sz)
sz: Prims.nat -> s: LowParse.Bytes.bytes{FStar.Seq.Base.length s == sz}
  -> FStar.Seq.Properties.lseq LowParse.Bytes.byte sz