The structure component index extractor , defined in this subsection, is used to get the numeric argument from a defined structure component extractor such as df-base (see ndxarg). For each defined structure component extractor, there should be a corresponding specific theorem providing its index, like basendx. The usage of these theorems, however, is discouraged since the particular value for the index is an implementation detail. It is generally sufficient to work with instead of the hard-coded index value, and use theorems such as baseid and basendxnplusgndx.
The main circumstance in which it is necessary to look at indices directly is when showing that a set of indices are disjoint (for example in proofs such as cznabel, based on setsnid) or even ordered (in proofs such as lmodstr). The requirement that the indices are distinct is necessary for sets of ordered pairs to be extensible structures, whereas the ordering allows for proofs avoiding the usage of quadradically many inequalities (compare cnfldfun with cnfldfunALT).
As for the inequalities, it is recommended to provide them explicitly as theorems like basendxnplusgndx, whenever they are required. Since these theorems use discouraged slot theorems, they should be placed near the definition of a slot (within the same subsection), so that the range of usages of discouraged theorems is tightly limited. Although there could be quadradically many of them in the total number of indices, much less are actually available (and not much more are expected).
As for the ordering, there are some theorems like basendxltplusgndx providing the less-than relationship between two indices. These theorems are also proved by discouraged theorems, so they should be placed near the definition of a slot (within the same subsection), too. However, since such theorems are rarely used (in structure building theorems *str like rngstr), it is not recommended to provide explicit theorems for all of them, but to use the (discouraged) *ndx theorems as in lmodstr. Therefore, *str theorems generally depend on the hard-coded values of the indices.