val t : Type0
let t = b:bool {b ==> model}
module MiTLS.Flags
open MiTLS

assume val model: bool // scaffolding
/
prims.fst.checked FStar.Pervasives.fsti.checked
MiTLS.Flags.fst
Type0
Prims.bool Prims.l_imp Prims.b2t MiTLS.Flags.model
let t =
  
b: bool{b ==> model}