val prefix (#a:Type) (s:seq a) (i:nat{i <= length s}): Tot (s':seq a{length s' = i})
val prefix (#a:Type) (s:seq a) (i:nat{i <= length s}): Tot (s':seq a{length s' = i})
let prefix (#a:Type) (s:seq a) (i:nat{i <= length s}) = slice s 0 i
module Zeta.SeqAux
#push-options "--print_universes"

open FStar.Classical
open FStar.Seq
open FStar.Squash
/
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}
  -> s': FStar.Seq.Base.seq a {FStar.Seq.Base.length s' = i}
FStar.Seq.Base.seq Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length FStar.Seq.Base.slice Prims.op_Equality
let prefix (#a: Type) (s: seq a) (i: nat{i <= length s}) =
  
slice s 0 i