  The key to any nameless representation of syntax is how it indicates the
variables we choose to use and thus, implicitly, those we discard. Standard de
Bruijn representations delay discarding maximally till the leaves of terms
where one is chosen from the variables in scope at the expense of the rest.
Consequently, introducing new but unused variables requires term traversal.
This paper introduces a nameless 'co-de-Bruijn' representation which makes the
opposite canonical choice, delaying discarding minimally, as near as possible
to the root. It is literate Agda: dependent types make it a practical joy to
express and be driven by strong intrinsic invariants which ensure that scope is
aggressively whittled down to just the support of each subterm, in which every
remaining variable occurs somewhere. The construction is generic, delivering a
universe of syntaxes with higher-order metavariables, for which the appropriate
notion of substitution is hereditary. The implementation of simultaneous
substitution exploits tight scope control to avoid busywork and shift terms
without traversal. Surprisingly, it is also intrinsically terminating, by
structural recursion alone.
