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