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