proposition: Lemma nodup_remdup : forall l, nodup (remdup l).
proof: Proof. induction l. simpl; auto. simpl. split. unfold not. apply notin_remove. eapply nodup_remove; eauto. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)