val lemma_flat_length_app1 (#a:Type) (ss: sseq a) (s: seq a)
  : Lemma (flat_length ss + length s = flat_length (append1 ss s))
val lemma_flat_length_app1 (#a:Type) (ss: sseq a) (s: seq a)
  : Lemma (flat_length ss + length s = flat_length (append1 ss s))
let lemma_flat_length_app1 (#a:Type) (ss: sseq a) (s: seq a)
  : Lemma (flat_length ss + length s = flat_length (append1 ss s)) =
  let ss' = append1 ss s in
  lemma_prefix1_append ss s;
  lemma_map_extend length ss';
  lemma_reduce_append 0 nat_add (map length ss) (length s);
  ()
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)

(* flat length of an empty sseq *)
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
/
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 -> s: FStar.Seq.Base.seq a
  -> FStar.Pervasives.Lemma
    (ensures
      Zeta.SSeq.flat_length ss + FStar.Seq.Base.length s =
      Zeta.SSeq.flat_length (Zeta.SeqAux.append1 ss s))
Zeta.SSeq.sseq FStar.Seq.Base.seq Prims.unit Zeta.SeqAux.lemma_reduce_append Prims.nat Zeta.SSeq.nat_add Zeta.SeqAux.map FStar.Seq.Base.length Zeta.SeqAux.lemma_map_extend Zeta.SeqAux.lemma_prefix1_append Prims.b2t Prims.op_Equality Prims.int Prims.op_Addition Zeta.SeqAux.append1 Prims.l_True Prims.squash Zeta.SSeq.flat_length Prims.Nil FStar.Pervasives.pattern
let lemma_flat_length_app1 (#a: Type) (ss: sseq a) (s: seq a)
    : Lemma (flat_length ss + length s = flat_length (append1 ss s)) =
  
let ss' = append1 ss s in
lemma_prefix1_append ss s;
lemma_map_extend length ss';
lemma_reduce_append 0 nat_add (map length ss) (length s);
()