fact: Definition forbid_specs (i : interface) : contract i unit := {| witness_update := const_witness ; caller_obligation := do_no_use ; callee_obligation := no_callee_obligation |}.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)