val 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))
        [SMTPat (index (prefix s i) j)]
val 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))
        [SMTPat (index (prefix s i) j)]
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
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 #_ _ _ = ()
/
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 -> i: Prims.nat{i <= FStar.Seq.Base.length s} -> j: Prims.nat{j < i}
  -> FStar.Pervasives.Lemma
      (ensures FStar.Seq.Base.index (Zeta.SeqAux.prefix s i) j == FStar.Seq.Base.index s j)
      [SMTPat (FStar.Seq.Base.index (Zeta.SeqAux.prefix s i) j)]
FStar.Seq.Base.seq Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.op_LessThan FStar.Seq.Base.lemma_index_slice Prims.unit Prims.l_True Prims.squash Prims.eq2 FStar.Seq.Base.index Zeta.SeqAux.prefix Prims.Nil FStar.Pervasives.pattern
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