proposition: Lemma Mlet_continuous_left : continuous (D1:=cDistr A) (D2:=(A-O->cDistr B) -M-> cDistr B) (MLet A B).
proof: Proof. red; intros; intro F; intro f. rewrite (MLet_simpl (A:=A) (B:=B)). simpl; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)