val seq_to_two_BE (#a: Type) (s: seq2 a) : two a
let seq_to_two_BE (#a:Type) (s:seq2 a) : two a =
  Mktwo (index s 1) (index s 0)
val seq_to_two_BE (#a: Type) (s: seq2 a) : two a
let seq_to_two_BE (#a: Type) (s: seq2 a) : two a =
Mktwo (index s 1) (index s 0)
Vale.Def.Words.Seq_s.fsti.checked
Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Words.Seq_s.fsti
Vale.Def.Words.Seq_s.seq2 Vale.Def.Words_s.Mktwo FStar.Seq.Base.index Vale.Def.Words_s.two
module Vale.Def.Words.Seq_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open FStar.Seq
open FStar.Mul
open Vale.Lib.Seqs_s

let seqn (n:nat) (a:Type) : Type = s:seq a{length s == n}
let seq2 (a:Type) = seqn 2 a
let seq4 (a:Type) = seqn 4 a
let seq8 (a:Type) = seqn 8 a
let seq16 (a:Type) = seqn 16 a

let seq_to_two_LE (#a:Type) (s:seq2 a) : two a =
  Mktwo (index s 0) (index s 1)
val seq_to_two_BE (#a: Type) (s: seq2 a) : two a
s: Vale.Def.Words.Seq_s.seq2 a -> Vale.Def.Words_s.two a