val prefix (#a #n: _) (il: interleaving a n) (i: nat{i <= length il}) : interleaving a n
val prefix (#a #n: _) (il: interleaving a n) (i: nat{i <= length il}) : interleaving a n
let prefix (#a:_) (#n:_) (il: interleaving a n) (i:nat{i <= length il})
  : interleaving a n
  = SA.prefix 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)
/
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: Prims.nat{i <= FStar.Seq.Base.length il}
  -> Zeta.Interleave.interleaving a n
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Zeta.Interleave.elem_src Zeta.SeqAux.prefix
let prefix (#a #n: _) (il: interleaving a n) (i: nat{i <= length il}) : interleaving a n =
  
SA.prefix il i