proposition: Theorem evalDist_iso : forall rel (A B C D : Set) (f : C -> D) (f_inv : D -> C) (d : Comp D) (c : Comp C) (f1 : D -> Comp B) (f2 : C -> Comp A) (a : A) (b : B), RatRel rel -> (forall x : D, In x (getSupport d) -> f (f_inv x) = x) -> (forall x : C, In x (getSupport c) -> f_inv (f x) = x) -> (forall x : D, In x (getSupport d) -> In (f_inv x) (getSupport c)) -> (forall x : C, In x (getSupport c) -> evalDist d (f x) == evalDist c x) -> (forall x : C, In x (getSupport c) -> rel (evalDist (f1 (f x)) b) (evalDist (f2 x) a)) -> rel (evalDist (x <-$ d; f1 x) b) (evalDist (x <-$ c; f2 x) a).
proof: Proof. intuition. eapply trans. eapply refl. eapply (distro_iso_eq); intros. eapply H0. trivial. eapply H1. eauto. eapply H2. eauto. eapply H3. trivial. eapply eqRat_refl. eapply rel_seq; intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms