proposition: Lemma forallb_false : forall l, forallb f l = false <-> exists x, In x l /\ f x = false.
proof: Proof. induction l; simpl. intuition. destruct H. intuition. rewrite andb_eq_false, IHl. intuition. exists a. tauto. destruct H0. exists x. tauto. destruct H1. intuition. subst. tauto. right. exists x. tauto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)