proposition: Theorem distro_irr_eq : forall (A B : Set)(b : Comp B)(a : B -> Comp A)(y : A) v, well_formed_comp b -> (forall x, In x (getSupport b) -> (evalDist (a x) y) == v) -> evalDist (Bind b a) y == v.
proof: Proof. intuition. simpl. rewrite sumList_body_eq. 2:{ intuition. rewrite H0 at 1. eapply eqRat_refl. trivial. } rewrite sumList_factor_constant_r. rewrite evalDist_lossless. eapply ratMult_1_l. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia