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

inline_for_extraction let model = false
/
prims.fst.checked FStar.Pervasives.fsti.checked
Model.Flags.fst
f: Model.Flags.ideal_flag{f ==> Model.Flags.ideal_TS}
let ideal_AEAD =
  
false