proposition: Theorem evalDist_seq_step : forall (A B :Set)(c : Comp A)(f : A -> Comp B) b, evalDist (Bind c f) b == sumList (getSupport c) (fun a => evalDist c a * evalDist (f a) b).
proof: Proof. intuition. simpl. eapply sumList_body_eq; intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia