proposition: Lemma nodup_intro' : forall l : list A, exists m p, l = m ++ p /\ nodup m.
proof: Proof. intro. ded (nodup_intro l). destruct H. exists l. exists nil. rewrite <- app_nil_end. auto. decomp H. exists x. exists (x0::x1). auto. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)