val create5_lseq (x0 x1 x2 x3 x4: uint64) : lseq uint64 5
let create5_lseq (x0 x1 x2 x3 x4:uint64) : lseq uint64 5 =
  let l = [x0; x1; x2; x3; x4] in
  assert_norm (FL.length l = 5);
  Seq.seq_of_list l
val create5_lseq (x0 x1 x2 x3 x4: uint64) : lseq uint64 5
let create5_lseq (x0 x1 x2 x3 x4: uint64) : lseq uint64 5 =
let l = [x0; x1; x2; x3; x4] in
assert_norm (FL.length l = 5);
Seq.seq_of_list l
Hacl.Spec.K256.PrecompTable.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.PrecompBaseTable.fsti.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Impl.K256.Point.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
Hacl.Spec.K256.PrecompTable.fst
Lib.IntTypes.uint64 FStar.Seq.Properties.seq_of_list Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int FStar.List.Tot.Base.length Prims.list Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.Cons Prims.Nil Lib.Sequence.lseq
module Hacl.Spec.K256.PrecompTable

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence

open Hacl.Spec.K256.Field52.Definitions
open Hacl.Impl.K256.Point

module S = Spec.K256
module FL = FStar.List.Tot
module SPT = Hacl.Spec.PrecompBaseTable

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val create5_lseq (x0 x1 x2 x3 x4: uint64) : lseq uint64 5

    x0: Lib.IntTypes.uint64 ->
    x1: Lib.IntTypes.uint64 ->
    x2: Lib.IntTypes.uint64 ->
    x3: Lib.IntTypes.uint64 ->
    x4: Lib.IntTypes.uint64
  -> Lib.Sequence.lseq Lib.IntTypes.uint64 5