proposition: Lemma nodup_remove (x : A) : forall l, nodup l -> nodup (remove eq_dec x l).
proof: Proof. induction l; simpl. auto. destruct (eq_dec a x). fo. simpl. fo. intro h. apply H. eapply incl_remove2. apply h. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)