fact: Definition instrument_to_state {i} `(ω : Ω) : instrument Ω i ~> state (semantics i) := fun a instr => fst <$> runStateT instr ω.
imports: ExtLib(StateMonad MonadTrans) FreeSpec.Core(Interface Semantics Contract)