proposition: Theorem evalDist_right_ident : forall (A : Set)(eqd : EqDec A)(c : Comp A) a, evalDist (x <-$ c; ret x) a == evalDist c a.
proof: Proof. intuition. destruct (in_dec (EqDec_dec eqd) a (getSupport c)). simpl. eapply eqRat_trans. eapply sumList_exactly_one. eapply getSupport_NoDup. eauto. intuition. destruct (EqDec_dec eqd b a). subst. intuition. eapply ratMult_0_r. destruct (EqDec_dec eqd a a). eapply ratMult_1_r. congruence. simpl. eapply eqRat_trans. eapply sumList_0. intuition. destruct (EqDec_dec eqd a0 a). subst. intuition. eapply ratMult_0_r. symmetry. eapply getSupport_not_In_evalDist. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia