val flat_length (#a:Type) (ss: sseq a)
  : Tot nat
val flat_length (#a:Type) (ss: sseq a)
  : Tot nat
let flat_length (#a:Type) (ss: sseq a):
  Tot nat =
  reduce 0 nat_add (map length ss)
module Zeta.SSeq

(* TODO: surely this should exists somewhere? *)
let nat_add (a b: nat): nat = a + b
/
Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.SSeq.fst
ss: Zeta.SSeq.sseq a -> Prims.nat
Zeta.SSeq.sseq Zeta.SeqAux.reduce Prims.nat Zeta.SSeq.nat_add Zeta.SeqAux.map FStar.Seq.Base.seq FStar.Seq.Base.length
let flat_length (#a: Type) (ss: sseq a) : Tot nat =
  
reduce 0 nat_add (map length ss)