val lemma_flat_length_empty (#a:Type)
  : Lemma (flat_length (empty #(seq a)) = 0)
val lemma_flat_length_empty (#a:Type)
  : Lemma (flat_length (empty #(seq a)) = 0)
let lemma_flat_length_empty (#a:Type):
  Lemma (flat_length (empty #(seq a)) = 0) =
  let empty_ss = empty #(seq a) in
  let lens = map length empty_ss in

  assert(length lens = 0);
  lemma_empty lens;
  lemma_reduce_empty 0 nat_add
module Zeta.SSeq

(* TODO: surely this should exists somewhere? *)
let nat_add (a b: nat): nat = a + b

(* sum of lengths of all sequences in a sequence of seqs *)
let flat_length (#a:Type) (ss: sseq a):
  Tot nat =
  reduce 0 nat_add (map length ss)
/
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
FStar.Pervasives.Lemma (ensures Zeta.SSeq.flat_length FStar.Seq.Base.empty = 0)
Zeta.SeqAux.lemma_reduce_empty Prims.nat Zeta.SSeq.nat_add Prims.unit FStar.Seq.Base.lemma_empty Prims._assert Prims.b2t Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Seq.Base.seq Zeta.SeqAux.map FStar.Seq.Base.empty Prims.l_True Prims.squash Zeta.SSeq.flat_length Prims.Nil FStar.Pervasives.pattern
let lemma_flat_length_empty (#a: Type) : Lemma (flat_length (empty #(seq a)) = 0) =
  
let empty_ss = empty #(seq a) in
let lens = map length empty_ss in
assert (length lens = 0);
lemma_empty lens;
lemma_reduce_empty 0 nat_add