proposition: Lemma notIn_filter : forall x l, ~In x (filter f l) <-> ~In x l \/ (In x l /\ f x = false).
proof: Proof. intros. rewrite filter_In. intuition. case (In_dec eq_dec x l); intro. right. intuition. revert H. case (f x). cong. refl. auto. rewrite H2 in H3. discr. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)