val four_to_two_two (#a: Type) (x: four a) : two (two a)
let four_to_two_two (#a:Type) (x:four a) : two (two a) =
  let Mkfour x0 x1 x2 x3 = x in
  Mktwo (Mktwo x0 x1) (Mktwo x2 x3)
val four_to_two_two (#a: Type) (x: four a) : two (two a)
let four_to_two_two (#a: Type) (x: four a) : two (two a) =
let Mkfour x0 x1 x2 x3 = x in
Mktwo (Mktwo x0 x1) (Mktwo x2 x3)
Vale.Def.Words.Four_s.fsti.checked
Vale.Def.Words_s.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Words.Four_s.fsti
Vale.Def.Words_s.four Vale.Def.Words_s.Mktwo Vale.Def.Words_s.two
module Vale.Def.Words.Four_s
open Vale.Def.Words_s
open FStar.Mul

unfold let four_map (#a #b:Type) (f:a -> b) (x:four a) : four b =
  let Mkfour x0 x1 x2 x3 = x in
  Mkfour (f x0) (f x1) (f x2) (f x3)

unfold let four_map2 (#a #b:Type) (f:a -> a -> b) (x y:four a) : four b =
  let Mkfour x0 x1 x2 x3 = x in
  let Mkfour y0 y1 y2 y3 = y in
  Mkfour (f x0 y0) (f x1 y1) (f x2 y2) (f x3 y3)

let two_two_to_four (#a:Type) (x:two (two a)) : four a =
  let (Mktwo (Mktwo x0 x1) (Mktwo x2 x3)) = x in
  Mkfour x0 x1 x2 x3
val four_to_two_two (#a: Type) (x: four a) : two (two a)
x: Vale.Def.Words_s.four a -> Vale.Def.Words_s.two (Vale.Def.Words_s.two a)