val index : il: Zeta.Interleave.interleaving a n -> i: Zeta.SeqAux.seq_index il -> a
let index (#a:_) (#n:_) (il: interleaving a n) (i: SA.seq_index il)
  = S.index (i_seq il) i
module Zeta.Interleave

open FStar.Seq
open Zeta.SeqAux
open Zeta.SSeq

module S = FStar.Seq
module SA = Zeta.SeqAux

type elem_src (a:eqtype) (n:nat) = {
  e: a;
  s: t:nat{t< n};
}

(* an interleaving of n sequences specifed by storing the mapping from every
 * interleaved element to the id of the src sequence *)
type interleaving (a:eqtype) (n:nat) = seq (elem_src a n)

unfold
let prefix (#a:_) (#n:_) (il: interleaving a n) (i:nat{i <= length il})
  : interleaving a n
  = SA.prefix il i

val i_seq (#a:_) (#n:nat) (il: interleaving a n)
  : is: seq a {length is = length il }

let src (#a:_) (#n:_) (il: interleaving a n) (i: SA.seq_index il)
  = (S.index il i).s
/
Zeta.SSeq.fsti.checked Zeta.SeqAux.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked
Zeta.Interleave.fsti
il: Zeta.Interleave.interleaving a n -> i: Zeta.SeqAux.seq_index il -> a
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Zeta.SeqAux.seq_index Zeta.Interleave.elem_src FStar.Seq.Base.index Zeta.Interleave.i_seq
let index (#a #n: _) (il: interleaving a n) (i: SA.seq_index il) =
  
S.index (i_seq il) i