val ideal_AEAD : f:ideal_flag{b2t f ==> b2t ideal_TS}
let ideal_AEAD = false
val ideal_AEAD : f:ideal_flag{b2t f ==> b2t ideal_TS}
let ideal_AEAD =
false
Model.Flags.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked
Model.Flags.fst
module Model.Flags

inline_for_extraction let model = false
val ideal_AEAD : f:ideal_flag{b2t f ==> b2t ideal_TS}
f: Model.Flags.ideal_flag{f ==> Model.Flags.ideal_TS}