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