proposition: Lemma Iin_mu_Iok : forall (A:Type) (I:IU) (e:Distr A) (F:A->IU) (f:A->U), (forall x, Iin (f x) (F x)) -> Iok I e F -> Iin (mu e f) I.
proof: Proof. intros; apply Iincl_in with (Imu e F); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)