val correct2 (#l: nat) (b:lbytes l)
  : Lemma (hide (reveal #l b) == b)
  [SMTPat (hide (reveal #l b))]
let correct2 #l b =
  assert (hide (reveal #l b) `Seq.equal` b)
val correct2 (#l: nat) (b:lbytes l)
  : Lemma (hide (reveal #l b) == b)
  [SMTPat (hide (reveal #l b))]
let correct2 #l b =
assert ((hide (reveal #l b)) `Seq.equal` b)
Model.Helpers.fst.checked
prims.fst.checked Lib.RawIntTypes.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Model.Helpers.fst
Prims.nat Model.Helpers.lbytes Prims._assert FStar.Seq.Base.equal Lib.IntTypes.uint8 Model.Helpers.hide Model.Helpers.reveal Prims.unit
module Model.Helpers

friend Lib.RawIntTypes

let correct #l (b:Seq.seq UInt8.t{Seq.length b = l})
  : Lemma (reveal #l (hide b) == b)
  [SMTPat (reveal #l (hide b))]
=
  assert (reveal #l (hide b) `Seq.equal` b)
val correct2 (#l: nat) (b:lbytes l)
  : Lemma (hide (reveal #l b) == b)
  [SMTPat (hide (reveal #l b))]
b: Model.Helpers.lbytes l
  -> FStar.Pervasives.Lemma (ensures Model.Helpers.hide (Model.Helpers.reveal b) == b)
      [SMTPat (Model.Helpers.hide (Model.Helpers.reveal b))]