proposition: Lemma pred_count_listRepeat_eq_inv : forall n (A : Type)(a : A) count, pred_count (eq a) (listRepeat a n) count -> count = n.
proof: Proof. induction n; intuition; simpl in *. inversion H. trivial. inversion H; clear H; subst. f_equal. eapply IHn; eauto. congruence. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation