proposition: Lemma Mon_law_1: forall (A B: Type) (v: A) (f: A -> mon B), run (Bind (Ret v) f) == run (f v).
proof: Proof. intros. rewrite run_Bind_Ret; apply eq_later. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)