proposition: Lemma Iapply_rule : forall (A B : Type) (a:Distr A) (f:A->Distr B)(I:IU)(F:A->IU)(G:B->IU), Iok I a F -> Iokfun F f (fun x => G) -> Iok I (Mlet a f) G.
proof: Proof. unfold Iokfun,Iok;intros. apply Ieq_incl_trans with (Imu a (fun x => Imu (f x) G0)); auto. apply Iincl_trans with (Imu a F); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)