val lemma_slices_le_quad32_to_bytes (q:quad32) : Lemma
  (ensures (
    let s = le_quad32_to_bytes q in
    q.lo0 == four_to_nat 8 (seq_to_four_LE (slice s 0 4)) /\
    q.lo1 == four_to_nat 8 (seq_to_four_LE (slice s 4 8)) /\
    q.hi2 == four_to_nat 8 (seq_to_four_LE (slice s 8 12)) /\
    q.hi3 == four_to_nat 8 (seq_to_four_LE (slice s 12 16))
  ))
let lemma_slices_le_quad32_to_bytes (q:quad32) : Lemma
  (ensures (
    let s = le_quad32_to_bytes q in
    q.lo0 == four_to_nat 8 (seq_to_four_LE (slice s 0 4)) /\
    q.lo1 == four_to_nat 8 (seq_to_four_LE (slice s 4 8)) /\
    q.hi2 == four_to_nat 8 (seq_to_four_LE (slice s 8 12)) /\
    q.hi3 == four_to_nat 8 (seq_to_four_LE (slice s 12 16))
  ))
  =
  reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
  reveal_opaque (`%le_quad32_to_bytes) le_quad32_to_bytes;
  ()
val lemma_slices_le_quad32_to_bytes (q:quad32) : Lemma
  (ensures (
    let s = le_quad32_to_bytes q in
    q.lo0 == four_to_nat 8 (seq_to_four_LE (slice s 0 4)) /\
    q.lo1 == four_to_nat 8 (seq_to_four_LE (slice s 4 8)) /\
    q.hi2 == four_to_nat 8 (seq_to_four_LE (slice s 8 12)) /\
    q.hi3 == four_to_nat 8 (seq_to_four_LE (slice s 12 16))
  ))
let lemma_slices_le_quad32_to_bytes (q: quad32)
    : Lemma
    (ensures
      (let s = le_quad32_to_bytes q in
        q.lo0 == four_to_nat 8 (seq_to_four_LE (slice s 0 4)) /\
        q.lo1 == four_to_nat 8 (seq_to_four_LE (slice s 4 8)) /\
        q.hi2 == four_to_nat 8 (seq_to_four_LE (slice s 8 12)) /\
        q.hi3 == four_to_nat 8 (seq_to_four_LE (slice s 12 16)))) =
reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
reveal_opaque (`%le_quad32_to_bytes) le_quad32_to_bytes;
()
Vale.AES.Types_helpers.fst.checked
Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.Types_helpers.fst
Vale.Def.Types_s.quad32 Prims.unit FStar.Pervasives.reveal_opaque FStar.Seq.Base.seq Vale.Def.Types_s.nat8 Prims.l_True Prims.eq2 Prims.int FStar.Seq.Base.length Vale.Def.Types_s.le_quad32_to_bytes Vale.Def.Words_s.four FStar.Mul.op_Star Vale.Def.Words.Seq_s.seq_four_to_seq_LE Prims.squash Prims.l_and Vale.Def.Words_s.natN Vale.Def.Words_s.pow2_32 Vale.Def.Words_s.__proj__Mkfour__item__lo0 Vale.Def.Types_s.nat32 Vale.Def.Words.Four_s.four_to_nat Vale.Def.Words.Seq_s.seq_to_four_LE FStar.Seq.Base.slice Vale.Def.Words_s.__proj__Mkfour__item__lo1 Prims.pow2 Vale.Def.Words_s.__proj__Mkfour__item__hi2 Vale.Def.Words_s.__proj__Mkfour__item__hi3 Vale.Def.Words_s.nat8 Prims.Nil FStar.Pervasives.pattern
module Vale.AES.Types_helpers

open Vale.Def.Words.Seq_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s
open Vale.Arch.Types
open FStar.Seq
open Vale.Arch.TypesNative

let lemma_slices_le_quad32_to_bytes (q:quad32) : Lemma
  (ensures (
    let s = le_quad32_to_bytes q in
    q.lo0 == four_to_nat 8 (seq_to_four_LE (slice s 0 4)) /\
    q.lo1 == four_to_nat 8 (seq_to_four_LE (slice s 4 8)) /\
    q.hi2 == four_to_nat 8 (seq_to_four_LE (slice s 8 12)) /\
    q.hi3 == four_to_nat 8 (seq_to_four_LE (slice s 12 16))
  ))
val lemma_slices_le_quad32_to_bytes (q:quad32) : Lemma
  (ensures (
    let s = le_quad32_to_bytes q in
    q.lo0 == four_to_nat 8 (seq_to_four_LE (slice s 0 4)) /\
    q.lo1 == four_to_nat 8 (seq_to_four_LE (slice s 4 8)) /\
    q.hi2 == four_to_nat 8 (seq_to_four_LE (slice s 8 12)) /\
    q.hi3 == four_to_nat 8 (seq_to_four_LE (slice s 12 16))
  ))
q: Vale.Def.Types_s.quad32
  -> FStar.Pervasives.Lemma
    (ensures
      (let s = Vale.Def.Types_s.le_quad32_to_bytes q in
        Mkfour?.lo0 q ==
        Vale.Def.Words.Four_s.four_to_nat 8
          (Vale.Def.Words.Seq_s.seq_to_four_LE (FStar.Seq.Base.slice s 0 4)) /\
        Mkfour?.lo1 q ==
        Vale.Def.Words.Four_s.four_to_nat 8
          (Vale.Def.Words.Seq_s.seq_to_four_LE (FStar.Seq.Base.slice s 4 8)) /\
        Mkfour?.hi2 q ==
        Vale.Def.Words.Four_s.four_to_nat 8
          (Vale.Def.Words.Seq_s.seq_to_four_LE (FStar.Seq.Base.slice s 8 12)) /\
        Mkfour?.hi3 q ==
        Vale.Def.Words.Four_s.four_to_nat 8
          (Vale.Def.Words.Seq_s.seq_to_four_LE (FStar.Seq.Base.slice s 12 16))))