proposition: Lemma run_Bind_Later: forall (A B: Type) (m: mon A) (f: A -> mon B), run (Bind (Later m) f) = later (run (Bind m f)).
proof: Proof. intros; samedelay. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)