val seq_index : s: FStar.Seq.Base.seq _ -> Type0
let seq_index = SA.seq_index
module Zeta.Interleave

open FStar.Classical
open Zeta.SeqIdx

module IF = Zeta.IdxFn
/
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
s: FStar.Seq.Base.seq _ -> Type0
Zeta.SeqAux.seq_index FStar.Seq.Base.seq
let seq_index =
  
SA.seq_index