val gen_seq : a: Prims.eqtype -> n: Prims.nat -> Zeta.IdxFn.gen_seq_spec
let gen_seq (a:eqtype) (n:_) =
  {
    IF.a = elem_src a n;
    IF.phi = (fun _ -> True);
    IF.phi_commutes_with_prefix = (fun _ _ -> ());
  }
module Zeta.Interleave

open FStar.Classical
open Zeta.SeqIdx

module IF = Zeta.IdxFn

let seq_index = SA.seq_index
/
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
a: Prims.eqtype -> n: Prims.nat -> Zeta.IdxFn.gen_seq_spec
Prims.eqtype Prims.nat Zeta.IdxFn.Mkgen_seq_spec Zeta.Interleave.elem_src FStar.Seq.Base.seq Prims.l_True Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.unit Zeta.IdxFn.gen_seq_spec
let gen_seq (a: eqtype) (n: _) =
  
{ IF.a = elem_src a n; IF.phi = (fun _ -> True); IF.phi_commutes_with_prefix = (fun _ _ -> ()) }