proposition: Lemma nodup_select (f : A->Prop) (f_dec : forall x, {f x}+{~f x}) : forall l, nodup l -> nodup (select f_dec l).
proof: Proof. induction l; simpl. fo. destruct (f_dec a); simpl; intuition. apply H0. eapply incl_select. apply H2. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)