proposition: Lemma nodup_intro: forall l : list A, nodup l \/ exists m x p, l = m ++ x :: p /\ nodup m /\ In x m.
proof: Proof. intro. ded (greatest_nodup_prefix_intro l). assert (nodup (greatest_nodup_prefix l)). apply greatest_nodup_prefix_correct. destruct H. left. rewrite H. exact H0. right. decomp H. ex (greatest_nodup_prefix l) x x0. intuition. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)