proposition: Lemma remdup_incl : forall l, remdup l [= l.
proof: Proof. induction l. simpl; unfold incl; auto. unfold incl; simpl. intros. destruct H. left; auto. right; apply IHl. eapply remove_In. eauto. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)