proposition: Lemma partition_complete : let p := partition f l in In a l -> In a (fst p) \/ In a (snd p).
proof: Proof. induction l. auto. simpl. intro. destruct (partition f l0). destruct H. destruct (f a0); simpl; auto. destruct (f a0); simpl in *; destruct IHl0; auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)