proposition: Lemma greatest_nodup_prefix_aux_correct : forall l acc, nodup acc -> nodup (greatest_nodup_prefix_aux acc l).
proof: Proof. induction l; simpl; intros. apply nodup_rev. exact H. case (In_dec eq_dec a acc); intro. apply nodup_rev. exact H. apply IHl. simpl. auto. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)