val hide_eq (b: Seq.seq UInt8.t)
    : Lemma (ensures hide b == QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b)
      [SMTPat (QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b)]
val hide_eq (b: Seq.seq UInt8.t)
    : Lemma (ensures hide b == QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b)
      [SMTPat (QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b)]
let hide_eq (b:Seq.seq UInt8.t) : Lemma
  (ensures hide b == QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b)
  [ SMTPat (QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b) ]
= 
  assert (hide b `Seq.equal` QUIC.Secret.Seq.seq_hide b)
module Model.Helpers

let lbytes (l:nat) = b:Seq.seq Lib.IntTypes.uint8 { Seq.length b = l }

let hide (b:Seq.seq UInt8.t) : lbytes (Seq.length b) =
  Seq.init (Seq.length b) (fun i -> Lib.RawIntTypes.u8_from_UInt8 (Seq.index b i))
/
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
b: FStar.Seq.Base.seq FStar.UInt8.t
  -> FStar.Pervasives.Lemma (ensures Model.Helpers.hide b == QUIC.Secret.Seq.seq_hide b)
      [SMTPat (QUIC.Secret.Seq.seq_hide b)]
FStar.Seq.Base.seq FStar.UInt8.t Prims._assert FStar.Seq.Base.equal Lib.IntTypes.uint8 Model.Helpers.hide QUIC.Secret.Seq.seq_hide Lib.IntTypes.U8 Prims.unit Prims.l_True Prims.squash Prims.eq2 Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Lib.IntTypes.uint_t Lib.IntTypes.SEC Prims.Nil
let hide_eq (b: Seq.seq UInt8.t)
    : Lemma (ensures hide b == QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b)
      [SMTPat (QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b)] =
  
assert ((hide b) `Seq.equal` (QUIC.Secret.Seq.seq_hide b))