val create4_lemma (x0 x1 x2 x3:uint64) :
  Lemma (let s = create4_lseq x0 x1 x2 x3 in
    s.[0] == x0 /\ s.[1] == x1 /\ s.[2] == x2 /\ s.[3] == x3)
let create4_lemma x0 x1 x2 x3 =
  Seq.elim_of_list [x0; x1; x2; x3]
val create4_lemma (x0 x1 x2 x3:uint64) :
  Lemma (let s = create4_lseq x0 x1 x2 x3 in
    s.[0] == x0 /\ s.[1] == x1 /\ s.[2] == x2 /\ s.[3] == x3)
let create4_lemma x0 x1 x2 x3 =
Seq.elim_of_list [x0; x1; x2; x3]
Hacl.Spec.P256.PrecompTable.fst.checked
Spec.P256.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.PrecompBaseTable256.fsti.checked Hacl.Spec.PrecompBaseTable.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Impl.P256.Point.fsti.checked Hacl.Impl.P256.Bignum.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Hacl.Spec.P256.PrecompTable.fst
Lib.IntTypes.uint64 FStar.Seq.Properties.elim_of_list Prims.Cons Prims.Nil Prims.unit
module Hacl.Spec.P256.PrecompTable

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

open Hacl.Impl.P256.Point

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery
module BD = Hacl.Spec.Bignum.Definitions
module FL = FStar.List.Tot
module SPT = Hacl.Spec.PrecompBaseTable

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

let create4_lseq (x0 x1 x2 x3:uint64) : lseq uint64 4 =
  let l = [x0; x1; x2; x3] in
  assert_norm (FL.length l = 4);
  Seq.seq_of_list l


val create4_lemma (x0 x1 x2 x3:uint64) :
  Lemma (let s = create4_lseq x0 x1 x2 x3 in
    s.[0] == x0 /\ s.[1] == x1 /\ s.[2] == x2 /\ s.[3] == x3)
val create4_lemma (x0 x1 x2 x3:uint64) :
  Lemma (let s = create4_lseq x0 x1 x2 x3 in
    s.[0] == x0 /\ s.[1] == x1 /\ s.[2] == x2 /\ s.[3] == x3)

    x0: Lib.IntTypes.uint64 ->
    x1: Lib.IntTypes.uint64 ->
    x2: Lib.IntTypes.uint64 ->
    x3: Lib.IntTypes.uint64
  -> FStar.Pervasives.Lemma
    (ensures
      (let s = Hacl.Spec.P256.PrecompTable.create4_lseq x0 x1 x2 x3 in
        s.[ 0 ] == x0 /\ s.[ 1 ] == x1 /\ s.[ 2 ] == x2 /\ s.[ 3 ] == x3))