val index_prefix_prop : gs: Zeta.SIdxFn.gen_sseq_base -> Prims.logical
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)
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;
}
/
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
gs: Zeta.SIdxFn.gen_sseq_base -> Prims.logical
Zeta.SIdxFn.gen_sseq_base Prims.l_Forall Zeta.IdxFn.seq_t Zeta.SIdxFn.__proj__Mkgen_sseq_base__item__gso Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Zeta.IdxFn.__proj__Mkgen_seq_spec__item__a Prims.op_LessThan Prims.op_Equality Zeta.SIdxFn.__proj__Mkgen_sseq_base__item__gsi Zeta.SIdxFn.__proj__Mkgen_sseq_base__item__index Zeta.SeqAux.prefix Prims.unit Zeta.IdxFn.__proj__Mkgen_seq_spec__item__phi_commutes_with_prefix Prims.logical
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)