val index_prop (#a #n:_) (il: interleaving a n) (i: SA.seq_index il)
  : Lemma (ensures ((S.index il i).e = index il i))
          [SMTPat (index il i)]
val index_prop (#a #n:_) (il: interleaving a n) (i: SA.seq_index il)
  : Lemma (ensures ((S.index il i).e = index il i))
          [SMTPat (index il i)]
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
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
/
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.SeqAux.seq_index il
  -> FStar.Pervasives.Lemma
      (ensures Mkelem_src?.e (FStar.Seq.Base.index il i) = Zeta.Interleave.index il i)
      [SMTPat (Zeta.Interleave.index il i)]
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Zeta.SeqAux.seq_index Zeta.Interleave.elem_src Zeta.IdxFn.lemma_map_map Zeta.Interleave.gen_seq Zeta.Interleave.to_elem Prims.unit Prims.l_True Prims.squash Prims.b2t Prims.op_Equality Zeta.Interleave.__proj__Mkelem_src__item__e FStar.Seq.Base.index Zeta.Interleave.index Prims.Nil FStar.Pervasives.pattern
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