proposition: Theorem evalDist_irr_r : forall (A B : Set)(c : Comp A)(f : A -> Comp B)(y : B) rel v, RatRel rel -> well_formed_comp c -> (forall x, In x (getSupport c) -> rel v (evalDist (f x) y)) -> rel v (evalDist (Bind c f) y).
proof: Proof. intuition. simpl. eapply trans. 2:{ eapply rel_sumList_compat; intuition. eapply mult_proper. eapply refl. eapply eqRat_refl. eapply H1. trivial. } specialize (rel_sumList_factor_r_r (evalDist c) (getSupport c) v H); intuition. eapply trans. 2:{ eapply H2. } eapply refl. rewrite evalDist_lossless. symmetry. eapply ratMult_1_l. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms