This paper explores a particular manner of dependently typed programming in which specifications stand in the foreground. Where possible, the program text concerns irrelevant proofs of propositions about relevant existential witnesses which are left implicit and inferred. In other words, the text is the explanation which provokes the mechanical construction of the part of the program that gets executed. The technique is put to work, in the context of syntax with binding, as a datatype-generic library for \emph{relevant} simultaneous substitution on codeBruijn syntax: terms are indexed by their \emph{support} of used variables, so they are $\alpha$-canonical on the nose and weakening composes thinnings instead of traversing terms. Substitutions and variable selections assemble into a thin double category. Instantiated to well-scoped System F, type substitution and term substitution are literally \emph{one} engine at two sorts, and a vacuous binder costs no substitution at all. An Agda implementation accompanies all the work presented herein.