proposition: Theorem evalDist_assoc : forall rel (A : Set)(c1 : Comp A)(B C : Set)(c2 : A -> Comp B)(c3 : B -> Comp C) x, RatRel rel -> rel (evalDist (Bind (Bind c1 c2) c3) x) (evalDist (Bind c1 (fun a => (Bind (c2 a) c3))) x).
proof: Proof. intuition. eapply refl. eapply evalDist_assoc_eq. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms