val parse32_flbytes_gen (sz: nat{sz < 4294967296}) (x: B32.lbytes sz)
    : Tot (y: B32.lbytes sz {y == parse_flbytes_gen sz (B32.reveal x)})
let parse32_flbytes_gen
  (sz: nat { sz < 4294967296 } )
  (x: B32.lbytes sz)
: Tot (y: B32.lbytes sz { y == parse_flbytes_gen sz (B32.reveal x) } )
= B32.hide_reveal x;
  x
val parse32_flbytes_gen (sz: nat{sz < 4294967296}) (x: B32.lbytes sz)
    : Tot (y: B32.lbytes sz {y == parse_flbytes_gen sz (B32.reveal x)})
let parse32_flbytes_gen (sz: nat{sz < 4294967296}) (x: B32.lbytes sz)
    : Tot (y: B32.lbytes sz {y == parse_flbytes_gen sz (B32.reveal x)}) =
B32.hide_reveal x;
x
LowParse.SLow.Bytes.fst.checked
prims.fst.checked LowParse.Spec.Bytes.fst.checked LowParse.SLow.VLGen.fst.checked LowParse.SLow.VLData.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
LowParse.SLow.Bytes.fst
Prims.nat Prims.b2t Prims.op_LessThan FStar.Bytes.lbytes Prims.unit FStar.Bytes.hide_reveal Prims.eq2 LowParse.Spec.Bytes.parse_flbytes_gen FStar.Bytes.reveal
module LowParse.SLow.Bytes
include LowParse.Spec.Bytes
include LowParse.SLow.VLData
include LowParse.SLow.VLGen

module B32 = FStar.Bytes
module Seq = FStar.Seq
module U32 = FStar.UInt32

inline_for_extraction
let parse32_flbytes_gen
  (sz: nat { sz < 4294967296 } )
  (x: B32.lbytes sz)
val parse32_flbytes_gen (sz: nat{sz < 4294967296}) (x: B32.lbytes sz)
    : Tot (y: B32.lbytes sz {y == parse_flbytes_gen sz (B32.reveal x)})
sz: Prims.nat{sz < 4294967296} -> x: FStar.Bytes.lbytes sz
  -> y: FStar.Bytes.lbytes sz {y == LowParse.Spec.Bytes.parse_flbytes_gen sz (FStar.Bytes.reveal x)}