proposition: Lemma Mext : forall (A:Type) (m:Distr A), Mlet m (fun x => Munit x) == m.
proof: Proof. intros; apply eq_distr_intro; simpl; intros. apply (mu_stable_eq m); simpl; apply ford_eq_intro; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)