val s_seq (#a:_) (#n:_) (il: interleaving a n): ss:sseq a{S.length ss = n}
val s_seq (#a:_) (#n:_) (il: interleaving a n): ss:sseq a{S.length ss = n}
let s_seq (#a:_) (#n:_) (il: interleaving a n)
  = init n (s_seq_i il)
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

let to_elem #a #n (il: interleaving a n) (i: seq_index il)
  = (S.index il i).e

let i_seq (#a:_) (#n:nat) (il: interleaving a n)
  = IF.map #(gen_seq a n) (to_elem #a #n) il

let index_prop (#a #n:_) (il: interleaving a n) (i: SA.seq_index il)
  : Lemma (ensures ((S.index il i).e = index il i))
  = IF.lemma_map_map #(gen_seq a n) #_ to_elem il i

let seq_i_fm (a:eqtype) n (i:nat)
  : IF.fm_t (gen_seq a n) a
  = IF.FM (from_src #a #n i) (to_elem #a #n)

let s_seq_i (#a:_) (#n:_) (il: interleaving a n) (i:nat{i < n})
  = IF.filter_map (seq_i_fm a n i) il
/
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 -> ss: Zeta.SSeq.sseq a {FStar.Seq.Base.length ss = n}
Prims.eqtype Prims.nat Zeta.Interleave.interleaving FStar.Seq.Base.init FStar.Seq.Base.seq Zeta.Interleave.s_seq_i Zeta.SSeq.sseq Prims.b2t Prims.op_Equality FStar.Seq.Base.length
let s_seq (#a #n: _) (il: interleaving a n) =
  
init n (s_seq_i il)