proposition: Theorem evalDist_commute: forall rel (A B : Set)(c1 : Comp A)(c2 : Comp B)(C : Set)(c3 : A -> B -> Comp C) x, RatRel rel -> rel (evalDist (a <-$ c1; b <-$ c2; (c3 a b)) x) (evalDist (b <-$ c2; a <-$ c1; (c3 a b)) x).
proof: Proof. intuition. eapply refl. eapply evalDist_commute_eq. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms