proposition: Lemma Mcomp : forall (A B C:Type) (m1: Distr A) (m2:A -> Distr B) (m3:B -> Distr C), Mlet (Mlet m1 m2) m3 == Mlet m1 (fun x:A => Mlet (m2 x) m3).
proof: Proof. intros; apply eq_distr_intro; intros; simpl; trivial. Qed.
imports: ALEA(Monads) ALEA(Utheory)