proposition: Lemma nodup_last : forall (a : A) l, nodup l -> ~In a l -> nodup (l ++ a :: nil).
proof: Proof. induction l; simpl; intros. auto. intuition. ded (in_app_or H). destruct H5. auto. simpl in H5. intuition. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)