proposition: Theorem evalDist_commute_eq : forall (A B : Set)(c1 : Comp A)(c2 : Comp B)(C : Set)(c3 : A -> B -> Comp C), dist_sem_eq (a <-$ c1; b <-$ c2; (c3 a b)) (b <-$ c2; a <-$ c1; (c3 a b)).
proof: Proof. intuition. unfold dist_sem_eq. intuition. simpl. eapply eqRat_trans. eapply sumList_body_eq. intuition. symmetry. eapply sumList_factor_constant_l. symmetry. eapply eqRat_trans. eapply sumList_body_eq. intuition. symmetry. eapply sumList_factor_constant_l. rewrite sumList_summation. eapply sumList_body_eq. intuition. eapply sumList_body_eq. intuition. repeat rewrite <- ratMult_assoc. eapply ratMult_eqRat_compat; intuition. eapply ratMult_comm. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia