val map_ghost
      (p: ('a -> Type0))
      (s: Seq.seq 'a {forall (i: Zeta.SeqAux.seq_index s). p (Seq.index s i)})
      (f: (x: 'a{p x} -> GTot 'b))
    : GTot
      (s':
        Seq.seq 'b
          { Seq.length s == Seq.length s' /\
            (forall (i: Zeta.SeqAux.seq_index s). Seq.index s' i == f (Seq.index s i)) })
      (decreases (Seq.length s))
val map_ghost
      (p: ('a -> Type0))
      (s: Seq.seq 'a {forall (i: Zeta.SeqAux.seq_index s). p (Seq.index s i)})
      (f: (x: 'a{p x} -> GTot 'b))
    : GTot
      (s':
        Seq.seq 'b
          { Seq.length s == Seq.length s' /\
            (forall (i: Zeta.SeqAux.seq_index s). Seq.index s' i == f (Seq.index s i)) })
      (decreases (Seq.length s))
let rec map_ghost (p:'a -> Type0) 
                  (s:Seq.seq 'a { forall (i:Zeta.SeqAux.seq_index s). p (Seq.index s i) })
                  (f: (x:'a { p x } -> GTot 'b))
  : GTot (s':Seq.seq 'b { Seq.length s == Seq.length s' /\
                         (forall (i:Zeta.SeqAux.seq_index s). Seq.index s' i == f (Seq.index s i)) })
         (decreases (Seq.length s))
  = if Seq.length s = 0 then Seq.empty
    else (
      let prefix, last = Seq.un_snoc s in
      Seq.snoc (map_ghost p prefix f) (f last)
    )
module Zeta.Steel.LogRel

module GV = Zeta.GenericVerifier
/
Zeta.Steel.Rel.fsti.checked Zeta.Steel.LogEntry.Types.fst.checked Zeta.SeqAux.fsti.checked Zeta.GenericVerifier.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.LogRel.fst

    p: (_: 'a -> Type0) ->
    s: FStar.Seq.Base.seq 'a {forall (i: Zeta.SeqAux.seq_index s). p (FStar.Seq.Base.index s i)} ->
    f: (x: 'a{p x} -> Prims.GTot 'b)
  -> Prims.GTot
    (s':
      FStar.Seq.Base.seq 'b
        { FStar.Seq.Base.length s == FStar.Seq.Base.length s' /\
          (forall (i: Zeta.SeqAux.seq_index s).
              FStar.Seq.Base.index s' i == f (FStar.Seq.Base.index s i)) })
FStar.Seq.Base.seq Prims.l_Forall Zeta.SeqAux.seq_index FStar.Seq.Base.index Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Seq.Base.empty Prims.bool FStar.Seq.Properties.snoc Zeta.Steel.LogRel.map_ghost Prims.l_and Prims.eq2 Prims.nat FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.fst FStar.Pervasives.Native.snd FStar.Seq.Properties.un_snoc
let rec map_ghost
      (p: ('a -> Type0))
      (s: Seq.seq 'a {forall (i: Zeta.SeqAux.seq_index s). p (Seq.index s i)})
      (f: (x: 'a{p x} -> GTot 'b))
    : GTot
      (s':
        Seq.seq 'b
          { Seq.length s == Seq.length s' /\
            (forall (i: Zeta.SeqAux.seq_index s). Seq.index s' i == f (Seq.index s i)) })
      (decreases (Seq.length s)) =
  
if Seq.length s = 0
then Seq.empty
else
  (let prefix, last = Seq.un_snoc s in
    Seq.snoc (map_ghost p prefix f) (f last))