proposition: Lemma Mif_eq : forall (A:Type)(b:(Distr bool))(f1 f2:Distr A)(q:MF A), mu (Mif b f1 f2) q == (mu f1 q) * (mu b ctrue) + (mu f2 q) * (mu b cfalse).
proof: Proof. intros. apply Oeq_trans with (mu b (fplus (fmult (mu f1 q) ctrue) (fmult (mu f2 q) cfalse))). intros; unfold Mif,Mlet,star; simpl. apply (mu_stable_eq b); simpl; apply ford_eq_intro; intro x. unfold fplus,fmult;destruct x; simpl. rewrite (Umult_one_right (mu f1 q)); rewrite (Umult_zero_right (mu f2 q)); auto. rewrite (Umult_zero_right (mu f1 q)); rewrite (Umult_one_right (mu f2 q)); auto. rewrite (mu_stable_plus b (f:=(fmult (mu f1 q) ctrue)) (g:=(fmult (mu f2 q) cfalse)) (ifok (mu f1 q) (mu f2 q))). rewrite (mu_stable_mult b (mu f1 q) ctrue). rewrite (mu_stable_mult b (mu f2 q) cfalse); trivial. Qed.
imports: ALEA(Probas) ALEA(Utheory)