proposition: Lemma nodup_app_cons : forall l (x : A) m, nodup (l ++ x :: m) -> ~In x l /\ ~In x m.
proof: Proof. split. apply nodup_rev in H. rewrite rev_app_distr in H. apply nodup_app_elim in H. decomp H. rewrite List.in_rev. apply H3. rewrite <- List.in_rev. simpl. auto. apply nodup_app_elim in H. simpl in H. tauto. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)