proposition: Lemma evalDist_in_f : forall (A B : Set)(c1 : Comp A)(c2 : Comp B)(f : A -> B), (forall a, eqRat (evalDist c1 a) (evalDist c2 (f a))) -> (forall a, In a (getSupport c1) <-> In (f a) (getSupport c2)).
proof: Proof. intros. specialize (getSupport_correct c1). specialize (getSupport_correct c2). intros. inversion H0; clear H0. inversion H1; clear H1. intuition. apply H3. intuition. eapply H4; eauto. eapply eqRat_trans. eapply H. eauto. eapply H4. intuition. eapply H3; eauto. eapply eqRat_trans. eapply eqRat_symm. eapply H. eauto. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia