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