proposition: Lemma Mon_law_2: forall (A: Type) (m: mon A), run (Bind m (@Ret A)) == run m.
proof: Proof. intros. eapply bisim_equi. apply Mon_law_2_aux. apply eta_match_1. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)