proposition: Lemma evalDist_getSupport_perm : forall (A B : Set)(c1 : Comp A)(c2 : Comp B) (f : A -> B)(f_inv : B -> A), (forall b, In b (getSupport c2) -> (f (f_inv b)) = b) -> (forall a, In a (getSupport c1) -> (f_inv (f a)) = a) -> (forall a, In a (getSupport c1) -> eqRat (evalDist c1 a) (evalDist c2 (f a))) -> (forall a, In a (getSupport c2) -> eqRat (evalDist c2 a) (evalDist c1 (f_inv a))) -> Permutation (map f (getSupport c1)) (getSupport c2).
proof: Proof. intuition. eapply NoDup_Permutation. eapply map_NoDup. intuition. eapply getSupport_NoDup. eapply getSupport_NoDup. intuition. apply in_map_iff in H3. destruct H3. intuition. subst. eapply getSupport_In_evalDist. intuition. eapply getSupport_In_evalDist. eauto. eapply eqRat_trans. eapply H1. trivial. trivial. eapply in_map_iff. econstructor. split. eapply H. trivial. eapply getSupport_In_evalDist. intuition. eapply getSupport_In_evalDist. eapply H3. rewrite H2. trivial. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia