val four_map2 (#a #b: Type) (f: (a -> a -> b)) (x y: four a) : four b
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)
val four_map2 (#a #b: Type) (f: (a -> a -> b)) (x y: four a) : four b
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)
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.Mkfour
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)
val four_map2 (#a #b: Type) (f: (a -> a -> b)) (x y: four a) : four b
f: (_: a -> _: a -> b) -> x: Vale.Def.Words_s.four a -> y: Vale.Def.Words_s.four a
  -> Vale.Def.Words_s.four b