val indexss (#a: Type) (ss: sseq a) (ij: sseq_index ss) : Tot a
val indexss (#a: Type) (ss: sseq a) (ij: sseq_index ss) : Tot a
let indexss (#a:Type) (ss: sseq a) (ij: sseq_index ss): Tot a =
  let (i,j) = ij in
  index (index ss i) j
module Zeta.SSeq

open FStar.Seq
open Zeta.SeqAux

(* sequence of sequences *)
type sseq (a:Type) = seq (seq a)

(* an index into an element of sseq *)
type sseq_index (#a:Type) (ss: sseq a) =
  (ij:(nat * nat){(fst ij) < length ss /\
               (snd ij) < length (index ss (fst ij))})
/
Zeta.SeqAux.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.SSeq.fsti
ss: Zeta.SSeq.sseq a -> ij: Zeta.SSeq.sseq_index ss -> a
Zeta.SSeq.sseq Zeta.SSeq.sseq_index Prims.nat FStar.Seq.Base.index FStar.Seq.Base.seq
let indexss (#a: Type) (ss: sseq a) (ij: sseq_index ss) : Tot a =
  
let i, j = ij in
index (index ss i) j