fact: Definition impure_lift `{Monad m} `(l : i ~> m) : impure i ~> m := fix aux a (p : impure i a) := match p with | local x => ret x | request_then e f => let* x := l _ e in aux a (f x) end.
imports: Coq(Program Setoid Morphisms)