proposition: Lemma partition_right : In a (snd (partition f l)) -> f a = false.
proof: Proof. induction l; simpl. intuition. destruct (partition f l0). destruct (bool_dec (f a0) true). rewrite e. apply IHl0. rewrite (not_true_is_false (f a0)). intro. destruct H. subst a0. destruct (f a); intuition. apply IHl0. hyp. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)