proposition: Lemma nodup_rev : forall l : list A, nodup l -> nodup (rev l).
proof: Proof. induction l; simpl; intros. exact H. destruct H. apply nodup_last. apply IHl. exact H0. intro. apply H. apply rev_incl. exact H1. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)