Some theorems about the library function index-of.
Theorem: index-of-nth-when-no-duplicatesp
(defthm index-of-nth-when-no-duplicatesp (implies (and (integer-range-p 0 (len x) i) (no-duplicatesp-equal x)) (equal (index-of (nth i x) x) i)))
