fact: CoFixpoint bind {A B: Type} (x: delay A) (f: A -> delay B) : delay B := match x with | now v => later (f v) | later y => later (bind y f) end.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)