fact: CoFixpoint run {A: Type} (m: mon A) : delay A := match m with | Ret v => now v | Later m => later (run m) | Bind (Ret v) f => later (run (f v)) | Bind (Later m) f => later (run (Bind m f)) | Bind (Bind m f) g => later (run (Bind m (fun x => Bind (f x) g))) end.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)