proposition: Lemma pred_count_permutation : forall (A : Set)(P : A -> Prop)(ls1 ls2 : list A), Permutation ls1 ls2 -> forall c, pred_count P ls1 c -> pred_count P ls2 c.
proof: Proof. induction 1; intuition. inversion H0; clear H0; subst. econstructor; eauto. econstructor; eauto. inversion H; clear H; subst. inversion H2; clear H2; subst. econstructor; eauto. econstructor; eauto. eapply pc_no; eauto. econstructor; eauto. inversion H2; clear H2; subst. econstructor; eauto. econstructor; eauto. econstructor; eauto. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation