let vale_alg_of_cipher_alg (a: cipher_alg { a == AES128 \/ a == AES256 }) =
  match a with
  | AES128 -> Vale.AES.AES_s.AES_128
  | AES256 -> Vale.AES.AES_s.AES_256
let vale_alg_of_cipher_alg (a: cipher_alg{a == AES128 \/ a == AES256}) =
match a with
| AES128 -> Vale.AES.AES_s.AES_128
| AES256 -> Vale.AES.AES_s.AES_256
Spec.Cipher.Expansion.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.AES.OptPublic.fsti.checked Vale.AES.AES_s.fst.checked Spec.Agile.Cipher.fsti.checked prims.fst.checked Lib.IntTypes.fst.checked Lib.IntTypes.fst.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Spec.Cipher.Expansion.fst
Spec.Agile.Cipher.cipher_alg Prims.l_or Prims.eq2 Spec.Agile.Cipher.AES128 Spec.Agile.Cipher.AES256 Vale.AES.AES_common_s.AES_128 Vale.AES.AES_common_s.AES_256 Vale.AES.AES_common_s.algorithm
module Spec.Cipher.Expansion

open Spec.Agile.Cipher

let vale_cipher_alg = a: cipher_alg { a == AES128 \/ a == AES256 }
val vale_alg_of_cipher_alg : a: Spec.Agile.Cipher.cipher_alg{a == Spec.Agile.Cipher.AES128 \/ a == Spec.Agile.Cipher.AES256}
  -> Vale.AES.AES_common_s.algorithm
a: Spec.Agile.Cipher.cipher_alg{a == Spec.Agile.Cipher.AES128 \/ a == Spec.Agile.Cipher.AES256}
  -> Vale.AES.AES_common_s.algorithm