proposition: Lemma incl_remdup : forall l, l [= remdup l.
proof: Proof. induction l. simpl; unfold incl; auto. unfold incl; simpl. intros. destruct (eq_dec a a0). auto. destruct H. auto. right. apply In_remove; auto. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)