proposition: Lemma nodup_unique : forall l (x:A), nodup l -> forall n m, l[n] = Some x -> l[m] = Some x -> n=m.
proof: Proof. intro; intro; induction l; intros; simpl in H; try discr. destruct n; destruct m; auto with *; simpl in *. rewrite <- H0 in H1; ded (element_at_in2 H1); tauto. rewrite <- H1 in H0; ded (element_at_in2 H0); tauto. destruct H; ded (IHl H2 n m H0 H1); auto. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)