proposition: Lemma pred_count_eq_all : forall (A : Type)(P : A -> Prop)(ls : list A) n, (forall a, In a ls -> P a) -> n = length ls -> pred_count P ls n.
proof: Proof. induction ls; intuition; simpl in *; subst. econstructor. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation