Variable binding, in its many forms, is ubiquitous in programming languages; therefore, approaches to representing binding structures and reasoning about them in theorem proving systems abound. We present a Coq library for reasoning about binding, based on a variant of Fiore, Plotkin and Turi’s notion of functorial syntax, and report on our experience in its development and use across a number of formalisation projects.