proposition: Theorem pred_count_eq_0 : forall (A B : Set)(ls : list B)(ls' : list A)(f : B -> A -> Prop)(P : A -> Prop) v, (forall a b, In b ls -> f b a -> ~ P a) -> rel_map f ls ls' -> pred_count P ls' v -> v = O.
proof: Proof. induction ls; intuition. inversion H0; subst; clear H0. inversion H1. trivial. inversion H0; clear H0; subst. inversion H1; clear H1; subst. exfalso. eapply H; eauto. simpl. intuition. eapply IHls; eauto. intuition. eapply H; eauto. simpl. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation