val append1 (#a: Type) (s: seq a) (x: a) : s': (seq a){length s' = length s + 1}
val append1 (#a: Type) (s: seq a) (x: a) : s': (seq a){length s' = length s + 1}
let append1 (#a:Type) (s:seq a) (x:a): s':(seq a){length s' = length s + 1} =
  append s (create 1 x)
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)

let telem (#a:Type) (s:seq a{length s > 0}): a =
  index 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 -> x: a
  -> s': FStar.Seq.Base.seq a {FStar.Seq.Base.length s' = FStar.Seq.Base.length s + 1}
FStar.Seq.Base.seq FStar.Seq.Base.append FStar.Seq.Base.create Prims.b2t Prims.op_Equality Prims.int FStar.Seq.Base.length Prims.op_Addition
let append1 (#a: Type) (s: seq a) (x: a) : s': (seq a){length s' = length s + 1} =
  
append s (create 1 x)