fact: Definition store_update (s : Type) := fun (x : s) (α : Type) (e : STORE s α) (_ : α) => match e with | Get => x | Put x' => x' end.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)