val lbytes : l: Prims.nat -> Type0
let lbytes (l:nat) = b:Seq.seq Lib.IntTypes.uint8 { Seq.length b = l }
module Model.Helpers
/
QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.RandomSequence.fsti.checked Lib.IntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked
Model.Helpers.fsti
l: Prims.nat -> Type0
Prims.nat FStar.Seq.Base.seq Lib.IntTypes.uint8 Prims.b2t Prims.op_Equality FStar.Seq.Base.length
let lbytes (l: nat) =
  
b: Seq.seq Lib.IntTypes.uint8 {Seq.length b = l}