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