proposition: Lemma evalDist_getSupport_perm_id : forall (A : Set)(c1 c2 : Comp A), (forall a, eqRat (evalDist c1 a) (evalDist c2 a)) -> Permutation (getSupport c1) (getSupport c2).
proof: Proof. intuition. rewrite <- map_id. eapply Permutation_sym. eapply evalDist_getSupport_perm; intuition. symmetry. eauto. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia