proposition: Lemma Imu_Mif_eq : forall (A:Type)(b:Distr bool)(f1 f2:Distr A)(F:A->IU), Ieq (Imu (Mif b f1 f2) F) (Iplus (Imultk (mu b ctrue) (Imu f1 F)) (Imultk (mu b cfalse) (Imu f2 F))).
proof: Proof. red; intros. rewrite low_Imu; rewrite up_Imu. repeat rewrite Mif_eq. repeat rewrite low_Iplus; repeat rewrite low_Imultk. repeat rewrite up_Iplus; repeat rewrite up_Imultk. repeat rewrite low_Imu; repeat rewrite up_Imu; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)