fact: Fixpoint with_semantics {ix j α} (sem : semantics j) (p : impure (ix + j) α) : impure ix α := match p with | local x => local x | request_then (in_right e) f => let (res, next) := run_effect sem e in with_semantics next (f res) | request_then (in_left e) f => request_then e (fun x => with_semantics sem (f x)) end.
imports: Coq(Program Setoid Morphisms) ExtLib(Monad StateMonad)