proposition: Theorem run_Bind: forall (A B: Type) (m: mon A) (f: A -> mon B), run (Bind m f) == bind (run m) (fun x => run (f x)).
proof: Proof. intros. change (Bind m f) with (Bind m (insert_cont (K0 _) f)). eapply equi_trans. apply run_Bind_aux. apply bind_context. apply Mon_law_2. intros; apply equi_refl. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)