val to_elem : il: Zeta.Interleave.interleaving a n -> i: Zeta.Interleave.seq_index il -> a
let to_elem #a #n (il: interleaving a n) (i: seq_index il)
  = (S.index il i).e
module Zeta.Interleave

open FStar.Classical
open Zeta.SeqIdx

module IF = Zeta.IdxFn

let seq_index = SA.seq_index

let gen_seq (a:eqtype) (n:_) =
  {
    IF.a = elem_src a n;
    IF.phi = (fun _ -> True);
    IF.phi_commutes_with_prefix = (fun _ _ -> ());
  }

(* an element is from src t *)
let from_src #a #n (t: nat) (il: interleaving a n) (i: seq_index il)
  = t = (S.index il i).s
/
Zeta.SSeq.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.IdxFn.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.Interleave.fst
il: Zeta.Interleave.interleaving a n -> i: Zeta.Interleave.seq_index il -> a
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Zeta.Interleave.seq_index Zeta.Interleave.elem_src Zeta.Interleave.__proj__Mkelem_src__item__e FStar.Seq.Base.index
let to_elem #a #n (il: interleaving a n) (i: seq_index il) =
  
(S.index il i).e