proposition: Lemma evalDist_getSupport_filter_perm : forall (A: Set)(c1 : Comp A)(c2 : Comp A)(P : A -> bool), (forall a, P a = true -> eqRat (evalDist c1 a) (evalDist c2 a)) -> Permutation (filter P (getSupport c1)) (filter P (getSupport c2)).
proof: Proof. intuition. eapply NoDup_Permutation. eapply filter_NoDup. eapply support_NoDup. eapply filter_NoDup. eapply support_NoDup. intuition. eapply filter_In in H0. eapply filter_In. intuition. eapply getSupport_In_evalDist. apply getSupport_In_evalDist in H1. intuition. apply H1. eapply eqRat_trans. eapply H. trivial. trivial. intuition. eapply filter_In in H0. eapply filter_In. intuition. eapply getSupport_In_evalDist. apply getSupport_In_evalDist in H1. intuition. apply H1. eapply eqRat_trans. eapply eqRat_symm. eapply H. trivial. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia