val lemma_fullprefix_equal (#a:Type) (s:seq a):
  Lemma (requires (True))
        (ensures (prefix s (length s) == s))
        [SMTPat (prefix s (length s))]
val lemma_fullprefix_equal (#a:Type) (s:seq a):
  Lemma (requires (True))
        (ensures (prefix s (length s) == s))
        [SMTPat (prefix s (length s))]
let lemma_fullprefix_equal (#a:Type) (s:seq a):
  Lemma (requires (True))
        (ensures (prefix s (length s) == s)) =
  let n = length s in
  let p = prefix s n in
  let aux (k:nat{k < n}):
    Lemma (index p k == index s k) =
    lemma_prefix_index s n k
  in
  forall_intro aux; lemma_eq_intro s p
module Zeta.SeqAux
#push-options "--print_universes"

open FStar.Classical
open FStar.Seq
open FStar.Squash

let prefix (#a:Type) (s:seq a) (i:nat{i <= length s}) = slice s 0 i

let prefix_slice #_ _ _ = ()

let lemma_prefix_index (#a:Type) (s:seq a) (i:nat{i <= length s}) (j:nat{j < i}):
  Lemma (requires (True))
        (ensures (index (prefix s i) j == index s j)) =
  lemma_index_slice s 0 i j

let lemma_prefix_prefix (#a:Type) (s:seq a) (i:nat{i <= length s}) (j:nat{j <= i}):
  Lemma (requires (True))
        (ensures (prefix (prefix s i) j == prefix s j)) =
  let pij = prefix (prefix s i) j in
  let pj = prefix s j in
  let pi = prefix s i in
  let aux (k:nat{k < j}):
    Lemma (index pij k == index pj k) =
    lemma_prefix_index s j k;
    lemma_prefix_index s i k;
    lemma_prefix_index pi j k
  in
  forall_intro aux; lemma_eq_intro pij pj
/
prims.fst.checked FStar.Squash.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.SeqAux.fst
s: FStar.Seq.Base.seq a
  -> FStar.Pervasives.Lemma (ensures Zeta.SeqAux.prefix s (FStar.Seq.Base.length s) == s)
      [SMTPat (Zeta.SeqAux.prefix s (FStar.Seq.Base.length s))]
FStar.Seq.Base.seq FStar.Seq.Base.lemma_eq_intro Prims.unit FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan Prims.eq2 FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Zeta.SeqAux.lemma_prefix_index Prims.op_Equality FStar.Seq.Base.length Zeta.SeqAux.prefix
let lemma_fullprefix_equal (#a: Type) (s: seq a)
    : Lemma (requires (True)) (ensures (prefix s (length s) == s)) =
  
let n = length s in
let p = prefix s n in
let aux (k: nat{k < n}) : Lemma (index p k == index s k) = lemma_prefix_index s n k in
forall_intro aux;
lemma_eq_intro s p