proposition: Lemma nodup_cut : forall (x : A) l, nodup l -> nodup (cut x l).
proof: Proof. induction l; simpl; intros. trivial. destruct (eq_dec x a). simpl. tauto. tauto. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)