fact: CoFixpoint derive_semantics {i j} (c : component i j) (sem : semantics j) : semantics i := mk_semantics (fun a p => let (res, next) := runState (to_state $ c a p) sem in (res, derive_semantics c next)).
imports: ExtLib(StateMonad)