proposition: Theorem evalDist_seq_eq_trans : forall (A B : Set) c1 c2 (f : A -> Comp B), (forall x, evalDist c1 x == evalDist c2 x) -> (forall x, evalDist (Bind c1 f) x == evalDist (Bind c2 f) x).
proof: Proof. intros. eapply evalDist_seq_eq; intuition idtac. reflexivity. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms