val gen_sseq : Type
let gen_sseq = gs: gen_sseq_base {index_prefix_prop gs}
module Zeta.SIdxFn

open FStar.Seq
open Zeta.SeqAux
open Zeta.SSeq
open Zeta.IdxFn

module S = FStar.Seq
module SA = Zeta.SeqAux
module SS = Zeta.SSeq

noeq
type gen_sseq_base = {

  (* outer sequence specification *)
  gso: gen_seq_spec;

  (* inner sequence specification *)
  gsi: gen_seq_spec;

  (* construct the inner sequence i *)
  index: s:seq_t gso -> i:nat{i < Seq.length s} -> seq_t gsi;
}

let index_prefix_prop (gs:gen_sseq_base)
  = forall (s:seq_t gs.gso) (j:nat{j <= Seq.length s}) (i: nat{i < j}).
    {:pattern gs.index (SA.prefix s j) i}
    (gs.gso.phi_commutes_with_prefix s j;
     gs.index (SA.prefix s j) i = gs.index s i)
/
Zeta.SSeq.fsti.checked Zeta.SeqAux.fsti.checked Zeta.IdxFn.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.SIdxFn.fsti
Type
Zeta.SIdxFn.gen_sseq_base Zeta.SIdxFn.index_prefix_prop
let gen_sseq =
  
gs: gen_sseq_base{index_prefix_prop gs}