val concat:
    #a:Type
  -> #len0:size_nat
  -> #len1:size_nat{len0 + len1 <= max_size_t}
  -> s0:lseq a len0
  -> s1:lseq a len1 ->
  Tot (s2:lseq a (len0 + len1){to_seq s2 == Seq.append (to_seq s0) (to_seq s1)})
let concat #a #len0 #len1 s0 s1 = Seq.append s0 s1
val concat:
    #a:Type
  -> #len0:size_nat
  -> #len1:size_nat{len0 + len1 <= max_size_t}
  -> s0:lseq a len0
  -> s1:lseq a len1 ->
  Tot (s2:lseq a (len0 + len1){to_seq s2 == Seq.append (to_seq s0) (to_seq s1)})
let concat #a #len0 #len1 s0 s1 =
Seq.append s0 s1
Lib.Sequence.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.Calc.fsti.checked
Lib.Sequence.fst
Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.max_size_t Lib.Sequence.lseq FStar.Seq.Base.append Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq
module Lib.Sequence

open FStar.Mul
open Lib.IntTypes
open Lib.LoopCombinators

#set-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0 --using_facts_from '-* +Prims +FStar.Pervasives +FStar.Math.Lemmas +FStar.Seq +Lib.IntTypes +Lib.Sequence'"

let index #a #len s n = Seq.index s n

let create #a len init = Seq.create #a len init
val concat:
    #a:Type
  -> #len0:size_nat
  -> #len1:size_nat{len0 + len1 <= max_size_t}
  -> s0:lseq a len0
  -> s1:lseq a len1 ->
  Tot (s2:lseq a (len0 + len1){to_seq s2 == Seq.append (to_seq s0) (to_seq s1)})
s0: Lib.Sequence.lseq a len0 -> s1: Lib.Sequence.lseq a len1
  -> s2:
    Lib.Sequence.lseq a (len0 + len1)
      { Lib.Sequence.to_seq s2 ==
        FStar.Seq.Base.append (Lib.Sequence.to_seq s0) (Lib.Sequence.to_seq s1) }