val lemma_slice_first_exactly_in_append (#a:Type) (x y:seq a) :
  Lemma (slice (append x y) 0 (length x) == x)
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_slice_first_exactly_in_append (#a:Type) (x y:seq a) :
  Lemma (slice (append x y) 0 (length x) == x)
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);
()
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.unit Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.slice FStar.Seq.Base.length FStar.Seq.Base.append Prims.l_True Prims.squash Prims.eq2 Prims.Nil FStar.Pervasives.pattern
module Vale.Lib.Seqs
open FStar.Mul
val lemma_slice_first_exactly_in_append (#a:Type) (x y:seq a) :
  Lemma (slice (append x y) 0 (length x) == x)
x: FStar.Seq.Base.seq a -> y: FStar.Seq.Base.seq a
  -> FStar.Pervasives.Lemma
    (ensures FStar.Seq.Base.slice (FStar.Seq.Base.append x y) 0 (FStar.Seq.Base.length x) == x)