The function iname is injective over the index.
Theorem: iname-injective-on-index
(defthm iname-injective-on-index (implies (stringp base) (equal (equal (iname base i) (iname base j)) (equal (nfix i) (nfix j)))))