val as_felem5_lseq (s: LSeq.lseq uint64 5) : felem5
let as_felem5_lseq (s:LSeq.lseq uint64 5) : felem5 =
  let open Lib.Sequence in
  (s.[0],s.[1],s.[2],s.[3],s.[4])
val as_felem5_lseq (s: LSeq.lseq uint64 5) : felem5
let as_felem5_lseq (s: LSeq.lseq uint64 5) : felem5 =
let open Lib.Sequence in (s.[ 0 ], s.[ 1 ], s.[ 2 ], s.[ 3 ], s.[ 4 ])
Hacl.Impl.K256.Point.fsti.checked
Spec.K256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.K256.Field.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Impl.K256.Point.fsti
Lib.Sequence.lseq Lib.IntTypes.uint64 FStar.Pervasives.Native.Mktuple5 Lib.Sequence.op_String_Access Hacl.Spec.K256.Field52.Definitions.felem5
module Hacl.Impl.K256.Point

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence

module S = Spec.K256
open Hacl.K256.Field

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

inline_for_extraction noextract
val as_felem5_lseq (s: LSeq.lseq uint64 5) : felem5
s: Lib.Sequence.lseq Lib.IntTypes.uint64 5 -> Hacl.Spec.K256.Field52.Definitions.felem5