val prefix (#gs: gen_seq_spec) (s: seq_t gs) (i: nat{i <= Seq.length s}) : seq_t gs
val prefix (#gs: gen_seq_spec) (s: seq_t gs) (i: nat{i <= Seq.length s}) : seq_t gs
let prefix (#gs:gen_seq_spec) (s:seq_t gs) (i:nat{i <= Seq.length s})
  : seq_t gs
  = gs.phi_commutes_with_prefix s i;
    SA.prefix s i
module Zeta.IdxFn

open FStar.Seq
open Zeta.SeqAux
module SA = Zeta.SeqAux

noeq
type gen_seq_spec = {
  a : eqtype;
  phi : Seq.seq a -> Type0;
  phi_commutes_with_prefix :
    s:Seq.seq a{phi s} ->
    i:nat{i <= Seq.length s} ->
    Lemma (phi (SA.prefix s i));
}

type seq_t (gs:gen_seq_spec) = s:Seq.seq gs.a{gs.phi s}
/
Zeta.SeqAux.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.IdxFn.fsti
s: Zeta.IdxFn.seq_t gs -> i: Prims.nat{i <= FStar.Seq.Base.length s} -> Zeta.IdxFn.seq_t gs
Zeta.IdxFn.gen_seq_spec Zeta.IdxFn.seq_t Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Zeta.IdxFn.__proj__Mkgen_seq_spec__item__a Zeta.SeqAux.prefix Prims.unit Zeta.IdxFn.__proj__Mkgen_seq_spec__item__phi_commutes_with_prefix
let prefix (#gs: gen_seq_spec) (s: seq_t gs) (i: nat{i <= Seq.length s}) : seq_t gs =
  
gs.phi_commutes_with_prefix s i;
SA.prefix s i