val nat_to_two (size: nat) (n: natN (pow2 (2 * size))) : two (natN (pow2 size))
let nat_to_two (size:nat) (n:natN (pow2 (2 * size))) : two (natN (pow2 size)) =
  nat_to_two_unfold size n
val nat_to_two (size: nat) (n: natN (pow2 (2 * size))) : two (natN (pow2 size))
let nat_to_two (size: nat) (n: natN (pow2 (2 * size))) : two (natN (pow2 size)) =
nat_to_two_unfold size n
Vale.Def.Words.Two_s.fsti.checked
Vale.Def.Words_s.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Words.Two_s.fsti
Prims.nat Vale.Def.Words_s.natN Prims.pow2 FStar.Mul.op_Star Vale.Def.Words.Two_s.nat_to_two_unfold Vale.Def.Words_s.two
module Vale.Def.Words.Two_s
open Vale.Def.Words_s
open FStar.Mul

unfold let two_map (#a #b:Type) (f:a -> b) (x:two a) : two b =
  let Mktwo x0 x1 = x in
  Mktwo (f x0) (f x1)

unfold let two_map2 (#a #b:Type) (f:a -> a -> b) (x y:two a) : two b =
  let Mktwo x0 x1 = x in
  let Mktwo y0 y1 = y in
  Mktwo (f x0 y0) (f x1 y1)

unfold
let nat_to_two_unfold (size:nat) (n:natN (pow2 (2 * size))) : two (natN (pow2 size)) =
  let n1 = pow2_norm size in
  let n2 = pow2_norm (2 * size) in
  Mktwo (n % n1) ((n / n1) % n1)
val nat_to_two (size: nat) (n: natN (pow2 (2 * size))) : two (natN (pow2 size))
size: Prims.nat -> n: Vale.Def.Words_s.natN (Prims.pow2 (2 * size))
  -> Vale.Def.Words_s.two (Vale.Def.Words_s.natN (Prims.pow2 size))