proposition: Lemma nodup_greatest_nodup_prefix : forall l, nodup l -> greatest_nodup_prefix l = l.
proof: Proof. induction l; simpl; intros. refl. destruct H. assert (l = l++nil). apply app_nil_end. rewrite H1. assert (forall x, In x l -> ~In x (a::nil)). simpl. intuition. subst a. auto. rewrite (greatest_nodup_prefix_aux_app nil H0 H2). simpl. rewrite rev_unit, rev_involutive, <- app_nil_end. refl. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)