proposition: Theorem evalDist_seq : forall rel (A1 A2 B : Set) (c1 c2 : Comp B) (f1 : B -> Comp A1)(f2 : B -> Comp A2) y z, RatRel rel -> (forall x : B, evalDist c1 x == evalDist c2 x) -> (forall x : B, In x (getSupport c1) -> rel (evalDist (f1 x) y) (evalDist (f2 x) z)) -> rel (evalDist (x <-$ c1; f1 x) y) (evalDist (x <-$ c2; f2 x) z).
proof: Proof. intuition. eapply (evalDist_iso (fun b => b)(fun b => b)); intuition. eapply getSupport_In_evalDist. intuition. eapply getSupport_In_evalDist. eauto. rewrite H0. trivial. eapply H1. eapply getSupport_In_evalDist. intuition. eapply getSupport_In_evalDist. eauto. rewrite <- H0. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms