proposition: Lemma evalDist_sum_bind_eq : forall (A B : Set)(eqdb : eq_dec B)(eqda : eq_dec A)(c1 : Comp B)(c2 : B -> Comp A), sumList (getSupport (Bind c1 c2)) (evalDist (Bind c1 c2)) == sumList (getSupport c1) (fun b => evalDist c1 b * (sumList (getSupport (c2 b)) (evalDist (c2 b)))).
proof: Proof. intuition. simpl. eapply eqRat_trans. eapply sumList_comm. eapply sumList_body_eq; intuition. eapply eqRat_trans. eapply sumList_factor_constant_l. eapply ratMult_eqRat_compat; intuition. eapply eqRat_symm. eapply sumList_subset; intuition. eapply getSupport_NoDup. eapply getUnique_NoDup. eapply (in_getUnique (flatten (map (fun b : B => getSupport (c2 b)) (getSupport c1)))). eapply in_flatten. econstructor. split. eapply in_map_iff. econstructor. split. eapply eq_refl. eauto. eauto. eapply getSupport_not_In_evalDist. eauto. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec