val lemma_expand_key_128_0 (key:aes_key_word AES_128) : Lemma
  (equal key (expand_key AES_128 key 4))
let lemma_expand_key_128_0 (key:aes_key_word AES_128) =
  expand_key_reveal ()
val lemma_expand_key_128_0 (key:aes_key_word AES_128) : Lemma
  (equal key (expand_key AES_128 key 4))
let lemma_expand_key_128_0 (key: aes_key_word AES_128) =
expand_key_reveal ()
Vale.AES.AES_helpers_BE.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.AES_BE_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Vale.AES.AES_helpers_BE.fst
Vale.AES.AES_BE_s.aes_key_word Vale.AES.AES_common_s.AES_128 Vale.AES.AES_BE_s.expand_key_reveal Prims.unit
module Vale.AES.AES_helpers_BE

open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Seq
open Vale.AES.AES_BE_s
open FStar.Mul

#reset-options "--fuel 4 --ifuel 0"
val lemma_expand_key_128_0 (key:aes_key_word AES_128) : Lemma
  (equal key (expand_key AES_128 key 4))
key: Vale.AES.AES_BE_s.aes_key_word Vale.AES.AES_common_s.AES_128
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Base.equal key (Vale.AES.AES_BE_s.expand_key Vale.AES.AES_common_s.AES_128 key 4))