proposition: Lemma greatest_nodup_prefix_aux_elim : forall l acc, exists p, greatest_nodup_prefix_aux acc l = rev acc ++ p.
proof: Proof. induction l; simpl; intros. exists nil. rewrite <- app_nil_end. refl. case (In_dec eq_dec a acc); intro. exists nil. rewrite <- app_nil_end. refl. ded (IHl (a::acc)). destruct H. rewrite H. simpl. rewrite app_ass. simpl. exists (a::x). refl. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)