val seq_map (#t1 #t2: Type) (f: (t1 -> Tot t2)) (x: seq t1)
    : Tot (lseq t2 (length x)) (decreases (length x))
val seq_map (#t1 #t2: Type) (f: (t1 -> Tot t2)) (x: seq t1)
    : Tot (lseq t2 (length x)) (decreases (length x))
let rec seq_map
  (#t1 #t2: Type)
  (f: (t1 -> Tot t2))
  (x: seq t1)
: Tot (lseq t2 (length x))
  (decreases (length x))
= if length x = 0
  then empty
  else cons (f (head x)) (seq_map f (tail x))
module QUIC.Secret.Seq
open FStar.Seq

module Secret = QUIC.Secret.Int
module U8 = FStar.UInt8
module Ghost = FStar.Ghost

(* NOTE: abstraction is NOT broken here *)
/
QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
QUIC.Secret.Seq.fst
f: (_: t1 -> t2) -> x: FStar.Seq.Base.seq t1
  -> Prims.Tot (FStar.Seq.Properties.lseq t2 (FStar.Seq.Base.length x))
FStar.Seq.Base.seq Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Seq.Base.empty Prims.bool FStar.Seq.Base.cons FStar.Seq.Properties.head QUIC.Secret.Seq.seq_map FStar.Seq.Properties.tail FStar.Seq.Properties.lseq
let rec seq_map (#t1 #t2: Type) (f: (t1 -> Tot t2)) (x: seq t1)
    : Tot (lseq t2 (length x)) (decreases (length x)) =
  
if length x = 0 then empty else cons (f (head x)) (seq_map f (tail x))