val lift_slots
      (s: Seq.seq s_slot_id {forall (i: Zeta.SeqAux.seq_index s). valid_slot (Seq.index s i)})
    : GTot
      (is:
        Seq.seq i_slot_id
          { Seq.length s = Seq.length is /\
            (forall i. related_slot (Seq.index s i) (Seq.index is i)) }) (decreases (Seq.length s))
val lift_slots
      (s: Seq.seq s_slot_id {forall (i: Zeta.SeqAux.seq_index s). valid_slot (Seq.index s i)})
    : GTot
      (is:
        Seq.seq i_slot_id
          { Seq.length s = Seq.length is /\
            (forall i. related_slot (Seq.index s i) (Seq.index is i)) }) (decreases (Seq.length s))
let lift_slots (s:Seq.seq s_slot_id { forall (i:Zeta.SeqAux.seq_index s). valid_slot (Seq.index s i)  })
  : GTot (is:Seq.seq i_slot_id  { Seq.length s = Seq.length is /\
                                  (forall i. related_slot (Seq.index s i) (Seq.index is i)) })
         (decreases (Seq.length s))
  = map_ghost (fun x -> valid_slot x) s lift_slot
module Zeta.Steel.LogRel

module GV = Zeta.GenericVerifier

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

    s:
      FStar.Seq.Base.seq Zeta.Steel.Rel.s_slot_id
        {forall (i: Zeta.SeqAux.seq_index s). Zeta.Steel.Rel.valid_slot (FStar.Seq.Base.index s i)}
  -> Prims.GTot
    (is:
      FStar.Seq.Base.seq Zeta.Steel.Rel.i_slot_id
        { FStar.Seq.Base.length s = FStar.Seq.Base.length is /\
          (forall (i: Prims.nat{i < FStar.Seq.Base.length s /\ i < FStar.Seq.Base.length is}).
              Zeta.Steel.Rel.related_slot (FStar.Seq.Base.index s i) (FStar.Seq.Base.index is i)) })
FStar.Seq.Base.seq Zeta.Steel.Rel.s_slot_id Prims.l_Forall Zeta.SeqAux.seq_index Prims.b2t Zeta.Steel.Rel.valid_slot FStar.Seq.Base.index Zeta.Steel.LogRel.map_ghost Zeta.Steel.Rel.i_slot_id Zeta.Steel.Rel.lift_slot Prims.l_and Prims.op_Equality Prims.nat FStar.Seq.Base.length Prims.op_LessThan Zeta.Steel.Rel.related_slot
let lift_slots
      (s: Seq.seq s_slot_id {forall (i: Zeta.SeqAux.seq_index s). valid_slot (Seq.index s i)})
    : GTot
      (is:
        Seq.seq i_slot_id
          { Seq.length s = Seq.length is /\
            (forall i. related_slot (Seq.index s i) (Seq.index is i)) }) (decreases (Seq.length s)) =
  
map_ghost (fun x -> valid_slot x) s lift_slot