val seq_gmap_index (#t1 #t2: Type) (f: (t1 -> GTot t2)) (x: seq t1) (i: nat{i < length x})
    : Lemma (ensures (index (seq_gmap f x) i == f (index x i)))
      (decreases (length x))
      [SMTPat (index (seq_gmap f x) i)]
val seq_gmap_index (#t1 #t2: Type) (f: (t1 -> GTot t2)) (x: seq t1) (i: nat{i < length x})
    : Lemma (ensures (index (seq_gmap f x) i == f (index x i)))
      (decreases (length x))
      [SMTPat (index (seq_gmap f x) i)]
let rec seq_gmap_index
  (#t1 #t2: Type)
  (f: (t1 -> GTot t2))
  (x: seq t1)
  (i: nat { i < length x })
: Lemma
  (ensures (index (seq_gmap f x) i == f (index x i)))
  (decreases (length x))
  [SMTPat (index (seq_gmap f x) i)]
= if i = 0
  then ()
  else seq_gmap_index f (tail x) (i - 1)
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 *)

noextract
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))

let rec seq_map_index
  (#t1 #t2: Type)
  (f: (t1 -> Tot t2))
  (x: seq t1)
  (i: nat { i < length x })
: Lemma
  (ensures (index (seq_map f x) i == f (index x i)))
  (decreases (length x))
  [SMTPat (index (seq_map f x) i)]
= if i = 0
  then ()
  else seq_map_index f (tail x) (i - 1)

let seq_hide
  #t x
= seq_map (Secret.cast t Secret.SEC) x

let seq_hide_length
  #t x
= ()

#push-options "--z3rlimit 32"

let seq_hide_index
  #t x i
= ()

#pop-options

noextract
let rec seq_gmap
  (#t1 #t2: Type)
  (f: (t1 -> GTot t2))
  (x: seq t1)
: GTot (lseq t2 (length x))
  (decreases (length x))
= if length x = 0
  then empty
  else cons (f (head x)) (seq_gmap f (tail x))
/
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 -> Prims.GTot t2) -> x: FStar.Seq.Base.seq t1 -> i: Prims.nat{i < FStar.Seq.Base.length x}
  -> FStar.Pervasives.Lemma
      (ensures FStar.Seq.Base.index (QUIC.Secret.Seq.seq_gmap f x) i == f (FStar.Seq.Base.index x i)
      )
      (decreases FStar.Seq.Base.length x)
      [SMTPat (FStar.Seq.Base.index (QUIC.Secret.Seq.seq_gmap f x) i)]
FStar.Seq.Base.seq Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Prims.op_Equality Prims.int Prims.bool QUIC.Secret.Seq.seq_gmap_index FStar.Seq.Properties.tail Prims.op_Subtraction Prims.unit Prims.l_True Prims.squash Prims.eq2 FStar.Seq.Base.index QUIC.Secret.Seq.seq_gmap Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let rec seq_gmap_index (#t1 #t2: Type) (f: (t1 -> GTot t2)) (x: seq t1) (i: nat{i < length x})
    : Lemma (ensures (index (seq_gmap f x) i == f (index x i)))
      (decreases (length x))
      [SMTPat (index (seq_gmap f x) i)] =
  
if i = 0 then () else seq_gmap_index f (tail x) (i - 1)