proposition: Lemma partition_inright : In a (snd (partition f l)) -> In a l.
proof: Proof. induction l. auto. simpl. intro. destruct (partition f l0). destruct (f a0). right. apply IHl0. auto. destruct H; auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)