My main use cases for manipulating indices directly are: (0) Implementing lexical contexts and environments whose variables are identified with de Bruijn indic

My main use cases for manipulating indices directly are: (0) Implementing lexical contexts and environments whose variables are identified with de Bruijn indices or levels. (1) Implementing multidimensional arrays and operations on them (e.g., matrix multiplication). In both of these cases, a solver for the theory of integer arithmetic can check that I'm using my indices right.