val lemma_append_extend (#a: Type) (s1: seq a) (s2: seq a {length s2 > 0})
    : Lemma (append s1 s2 == append1 (append s1 (hprefix s2)) (telem s2))
val lemma_append_extend (#a: Type) (s1: seq a) (s2: seq a {length s2 > 0})
    : Lemma (append s1 s2 == append1 (append s1 (hprefix s2)) (telem s2))
let lemma_append_extend (#a:Type) (s1: seq a) (s2: seq a{length s2 > 0}):
  Lemma (append s1 s2 == append1 (append s1 (hprefix s2)) (telem s2)) =
  let s2' = hprefix s2 in
  let e2 = telem s2 in
  let aux (i: seq_index (append s1 s2)):
    Lemma (requires True)
          (ensures (index (append s1 s2) i == index (append1 (append s1 s2') e2) i))
          [SMTPat (index (append1 (append s1 s2') e2) i)] = ()
  in
  assert(equal (append s1 s2) (append1 (append s1 s2') e2));
  ()
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

(* appending a singleton adds to the flat length *)
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);
  ()
/
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
s1: FStar.Seq.Base.seq a -> s2: FStar.Seq.Base.seq a {FStar.Seq.Base.length s2 > 0}
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Base.append s1 s2 ==
      Zeta.SeqAux.append1 (FStar.Seq.Base.append s1 (Zeta.SeqAux.hprefix s2)) (Zeta.SeqAux.telem s2)
    )
FStar.Seq.Base.seq Prims.b2t Prims.op_GreaterThan FStar.Seq.Base.length Prims.unit Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.append Zeta.SeqAux.append1 Zeta.SeqAux.seq_index Prims.l_True Prims.squash Prims.eq2 FStar.Seq.Base.index Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil Zeta.SeqAux.telem Zeta.SeqAux.hprefix
let lemma_append_extend (#a: Type) (s1: seq a) (s2: seq a {length s2 > 0})
    : Lemma (append s1 s2 == append1 (append s1 (hprefix s2)) (telem s2)) =
  
let s2' = hprefix s2 in
let e2 = telem s2 in
let aux (i: seq_index (append s1 s2))
    : Lemma (requires True)
      (ensures (index (append s1 s2) i == index (append1 (append s1 s2') e2) i))
      [SMTPat (index (append1 (append s1 s2') e2) i)] =
  ()
in
assert (equal (append s1 s2) (append1 (append s1 s2') e2));
()