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