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