val two_to_seq_BE (#a:Type) (x:two a) : Pure (seq2 a)
  (requires True)
  (ensures fun s ->
    index s 1 == x.lo /\
    index s 0 == x.hi
  )
let two_to_seq_BE #a x =
  let l = [x.hi; x.lo] in
  let s = seq_of_list l in
  lemma_seq_of_list_index l 0;
  lemma_seq_of_list_index l 1;
  seq_of_list l
val two_to_seq_BE (#a:Type) (x:two a) : Pure (seq2 a)
  (requires True)
  (ensures fun s ->
    index s 1 == x.lo /\
    index s 0 == x.hi
  )
let two_to_seq_BE #a x =
let l = [x.hi; x.lo] in
let s = seq_of_list l in
lemma_seq_of_list_index l 0;
lemma_seq_of_list_index l 1;
seq_of_list l
Vale.Def.Words.Seq_s.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Words.Seq_s.fst
Vale.Def.Words_s.two FStar.Seq.Properties.seq_of_list Prims.unit FStar.Seq.Properties.lemma_seq_of_list_index FStar.Seq.Base.seq Prims.b2t Prims.op_Equality Prims.nat FStar.List.Tot.Base.length FStar.Seq.Base.length Prims.list Prims.Cons Vale.Def.Words_s.__proj__Mktwo__item__hi Vale.Def.Words_s.__proj__Mktwo__item__lo Prims.Nil Vale.Def.Words.Seq_s.seq2
module Vale.Def.Words.Seq_s
open FStar.Mul

#reset-options "--max_fuel 3 --initial_fuel 3"
let two_to_seq_LE #a x =
  let l = [x.lo; x.hi] in
  let s = seq_of_list l in
  lemma_seq_of_list_index l 0;
  lemma_seq_of_list_index l 1;
  seq_of_list l
val two_to_seq_BE (#a:Type) (x:two a) : Pure (seq2 a)
  (requires True)
  (ensures fun s ->
    index s 1 == x.lo /\
    index s 0 == x.hi
  )
x: Vale.Def.Words_s.two a -> Prims.Pure (Vale.Def.Words.Seq_s.seq2 a)