val lemma_all_but_last_append (#t:Type) (a:seq t) (b:seq t{length b > 0}) :
  Lemma (all_but_last (append a b) == append a (all_but_last b))
let lemma_all_but_last_append (#t:Type) (a:seq t) (b:seq t{length b > 0}) :
  Lemma (all_but_last (append a b) == append a (all_but_last b)) =
  let ab = all_but_last (append a b) in
  let app_a_b = append a (all_but_last b) in
  assert (equal ab app_a_b)
val lemma_all_but_last_append (#t:Type) (a:seq t) (b:seq t{length b > 0}) :
  Lemma (all_but_last (append a b) == append a (all_but_last b))
let lemma_all_but_last_append (#t: Type) (a: seq t) (b: seq t {length b > 0})
    : Lemma (all_but_last (append a b) == append a (all_but_last b)) =
let ab = all_but_last (append a b) in
let app_a_b = append a (all_but_last b) in
assert (equal ab app_a_b)
Vale.Lib.Seqs.fst.checked
prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.Calc.fsti.checked
Vale.Lib.Seqs.fst
FStar.Seq.Base.seq Prims.b2t Prims.op_GreaterThan FStar.Seq.Base.length Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.append Vale.Lib.Seqs_s.all_but_last Prims.unit Prims.l_True Prims.squash Prims.eq2 Prims.Nil FStar.Pervasives.pattern
module Vale.Lib.Seqs
open FStar.Mul

let lemma_slice_first_exactly_in_append (#a:Type) (x y:seq a) :
  Lemma (slice (append x y) 0 (length x) == x) =
  let xy = append x y in
  let xy_slice = slice xy 0 (length x) in
  let x_slice = slice x 0 (length x) in
  assert(equal xy_slice x_slice);   // OBSERVE: extensionality
  ()
val lemma_all_but_last_append (#t:Type) (a:seq t) (b:seq t{length b > 0}) :
  Lemma (all_but_last (append a b) == append a (all_but_last b))
a: FStar.Seq.Base.seq t -> b: FStar.Seq.Base.seq t {FStar.Seq.Base.length b > 0}
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.Lib.Seqs_s.all_but_last (FStar.Seq.Base.append a b) ==
      FStar.Seq.Base.append a (Vale.Lib.Seqs_s.all_but_last b))