val bytes_equal (b1 b2: bytes) : GTot Type0
let bytes_equal (b1 b2: bytes) : GTot Type0 =
  Seq.length b1 == Seq.length b2 /\
  (forall (i: nat { i < Seq.length b1 } ) . {:pattern (Seq.index b1 i); (Seq.index b2 i) } U8.v (Seq.index b1 i) == U8.v (Seq.index b2 i))
val bytes_equal (b1 b2: bytes) : GTot Type0
let bytes_equal (b1 b2: bytes) : GTot Type0 =
Seq.length b1 == Seq.length b2 /\
(forall (i: nat{i < Seq.length b1}). {:pattern (Seq.index b1 i); (Seq.index b2 i)}
    U8.v (Seq.index b1 i) == U8.v (Seq.index b2 i))
LowParse.Bytes.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
LowParse.Bytes.fst
LowParse.Bytes.bytes Prims.l_and Prims.eq2 Prims.nat FStar.Seq.Base.length LowParse.Bytes.byte Prims.l_Forall Prims.b2t Prims.op_LessThan FStar.UInt.uint_t FStar.UInt8.n FStar.UInt8.v FStar.Seq.Base.index
module LowParse.Bytes

module Seq = FStar.Seq
module U8 = FStar.UInt8
val bytes_equal (b1 b2: bytes) : GTot Type0
b1: LowParse.Bytes.bytes -> b2: LowParse.Bytes.bytes -> Prims.GTot Type0