val four_to_seq_LE (#a:Type) (x:four a) : Pure (seq4 a)
  (requires True)
  (ensures fun s ->
    index s 0 == x.lo0 /\
    index s 1 == x.lo1 /\
    index s 2 == x.hi2 /\
    index s 3 == x.hi3
  )
let four_to_seq_LE #a x =
  let l = [x.lo0; x.lo1; x.hi2; x.hi3] in
  let s = seq_of_list l in
  lemma_seq_of_list_index l 0;
  lemma_seq_of_list_index l 1;
  lemma_seq_of_list_index l 2;
  lemma_seq_of_list_index l 3;
  seq_of_list l
val four_to_seq_LE (#a:Type) (x:four a) : Pure (seq4 a)
  (requires True)
  (ensures fun s ->
    index s 0 == x.lo0 /\
    index s 1 == x.lo1 /\
    index s 2 == x.hi2 /\
    index s 3 == x.hi3
  )
let four_to_seq_LE #a x =
let l = [x.lo0; x.lo1; x.hi2; x.hi3] in
let s = seq_of_list l in
lemma_seq_of_list_index l 0;
lemma_seq_of_list_index l 1;
lemma_seq_of_list_index l 2;
lemma_seq_of_list_index l 3;
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.four 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__Mkfour__item__lo0 Vale.Def.Words_s.__proj__Mkfour__item__lo1 Vale.Def.Words_s.__proj__Mkfour__item__hi2 Vale.Def.Words_s.__proj__Mkfour__item__hi3 Prims.Nil Vale.Def.Words.Seq_s.seq4
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

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
#reset-options
val four_to_seq_LE (#a:Type) (x:four a) : Pure (seq4 a)
  (requires True)
  (ensures fun s ->
    index s 0 == x.lo0 /\
    index s 1 == x.lo1 /\
    index s 2 == x.hi2 /\
    index s 3 == x.hi3
  )
x: Vale.Def.Words_s.four a -> Prims.Pure (Vale.Def.Words.Seq_s.seq4 a)