proposition: Lemma nodup_shrink : forall l : list A, nodup (shrink l).
proof: Proof. induction l; simpl; intros. trivial. destruct (In_dec eq_dec a (shrink l)). apply nodup_cut. hyp. simpl. tauto. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)