let v_inttype = t:inttype{unsigned t /\ ~(U1? t)}
let v_inttype =
t: inttype{unsigned t /\ ~(U1? t)}
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.inttype Prims.l_and Prims.b2t Lib.IntTypes.unsigned Prims.l_not Lib.IntTypes.uu___is_U1
module Lib.IntVector

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

#set-options "--z3rlimit 20 --max_fuel 0 --max_ifuel 0"
val v_inttype : Type0
Type0