proposition: Lemma Iifrule : forall (A:Type)(b:(Distr bool))(f1 f2:Distr A)(I1 I2:IU)(F:A->IU), Iok I1 f1 F -> Iok I2 f2 F -> Iok (Iplus (Imultk (mu b ctrue) I1) (Imultk (mu b cfalse) I2)) (Mif b f1 f2) F.
proof: Proof. unfold Iok; intros. apply Ieq_incl_trans with (1:=Imu_Mif_eq b f1 f2 F). split. repeat rewrite low_Iplus; repeat rewrite low_Imultk. apply Uplus_le_compat; auto. repeat rewrite up_Iplus; repeat rewrite up_Imultk. apply Uplus_le_compat; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)