proposition: Lemma greatest_nodup_prefix_aux_app : forall m l acc, nodup l -> (forall x, In x l -> ~In x acc) -> greatest_nodup_prefix_aux acc (l ++ m) = greatest_nodup_prefix_aux (rev l ++ acc) m.
proof: Proof. induction l; simpl; intros. refl. destruct H. case (In_dec eq_dec a acc); intro. absurd (In a acc). apply H0. auto. exact i. assert (forall x, In x l -> ~In x (a::acc)). intuition. destruct H3. subst a. auto. eapply H0. right. apply H2. exact H3. rewrite (IHl (a::acc) H1 H2). rewrite app_ass. refl. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)