Theorem: member-equal-of-iname-and-iname-list
(defthm member-equal-of-iname-and-iname-list (implies (stringp base) (iff (member-equal (iname base i) (iname-list base n)) (< (nfix i) (nfix n)))))