let nat16 = Vale.Def.Words_s.nat16
let nat16 =
Vale.Def.Words_s.nat16
Vale.Def.Types_s.fst.checked
Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Types_s.fst
Vale.Def.Words_s.nat16
module Vale.Def.Types_s

open FStar.Mul
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.Def.Words.Seq_s
open FStar.Seq
open Vale.Lib.Seqs_s
val nat16 : Type0
Type0