fact: Fixpoint impure_bind {i α β} (p : impure i α) (f : α -> impure i β) : impure i β := match p with | local x => f x | request_then e g => request_then e (fun x => impure_bind (g x) f) end.
imports: Coq(Program Setoid Morphisms)