We present CARVe (‘Contexts as Resource Vectors’), a Rocq library for mechanizing substructural logics and languages. CARVe represents resource usage algebraically, eliminating the need for explicit context splitting and complex re-indexing. This approach integrates smoothly with well-scoped de Bruijn syntax, simplifying formalizations of linear, affine and other substructural systems.