let felem4 = (uint64 * uint64 * uint64 * uint64)
let felem4 =
(((uint64 * uint64) * uint64) * uint64)
Hacl.Spec.Curve25519.Field64.Definition.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Impl.Curve25519.Lemmas.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.Curve25519.Field64.Definition.fst
FStar.Pervasives.Native.tuple4 Lib.IntTypes.uint64
module Hacl.Spec.Curve25519.Field64.Definition

open Lib.Sequence
open Lib.IntTypes

module P = Spec.Curve25519

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val felem4 : Type0
Type0