proposition: Lemma pred_count_func : forall (A : Type)(P : A -> Prop)(ls : list A) n1 n2, pred_count P ls n1 -> pred_count P ls n2 -> n1 = n2.
proof: Proof. induction ls; intuition. inversion H. inversion H0. trivial. inversion H; clear H; subst. inversion H0; clear H0; subst. f_equal. eapply IHls; eauto. intuition. inversion H0; clear H0; subst. intuition. eapply IHls; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation