val telem (#a: Type) (s: seq a {length s > 0}) : a
val telem (#a: Type) (s: seq a {length s > 0}) : a
let telem (#a:Type) (s:seq a{length s > 0}): a =
  index s (length s - 1)
module Zeta.SeqAux

open FStar.Seq

(* Legitimate values of an index of a sequence *)
inline_for_extraction
type seq_index (#a:Type) (s:seq a) = i:nat{i < length s}

(* Prefix of a sequence *)
val prefix (#a:Type) (s:seq a) (i:nat{i <= length s}): Tot (s':seq a{length s' = i})

let hprefix (#a:Type) (s:seq a{length s > 0}): seq a = 
  prefix s (length s - 1)
/
prims.fst.checked FStar.Squash.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.SeqAux.fsti
s: FStar.Seq.Base.seq a {FStar.Seq.Base.length s > 0} -> a
FStar.Seq.Base.seq Prims.b2t Prims.op_GreaterThan FStar.Seq.Base.length FStar.Seq.Base.index Prims.op_Subtraction
let telem (#a: Type) (s: seq a {length s > 0}) : a =
  
index s (length s - 1)