let width = n:size_nat{n == 1 \/ n == 2 \/ n == 4 \/ n == 8 \/ n == 16 \/ n == 32}
let width =
n: size_nat{n == 1 \/ n == 2 \/ n == 4 \/ n == 8 \/ n == 16 \/ n == 32}
Lib.IntVector.fsti.checked
Spec.AES.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Lib.IntVector.fsti
Lib.IntTypes.size_nat Prims.l_or Prims.eq2 Prims.int
module Lib.IntVector

open FStar.Mul
open Lib.Sequence
open Lib.IntTypes

#set-options "--z3rlimit 20 --max_fuel 0 --max_ifuel 0"

let v_inttype = t:inttype{unsigned t /\ ~(U1? t)}
val width : Type0
Type0