proposition: Lemma let_indep : forall (A B:Type) (m1:Distr A) (m2: Distr B) (f:MF B), mu m1 (fun _ => mu m2 f) == mu m1 (fone A) * (mu m2 f).
proof: Proof. intros; rewrite (mu_cte m1 (mu m2 f)); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)