fact: Definition to_instrument `{MayProvide ix i} `(c : contract i Ω) : impure ix ~> instrument Ω ix := impure_lift $ interface_to_instrument c.
imports: ExtLib(StateMonad MonadTrans) FreeSpec.Core(Interface Semantics Contract)