When reasoning about properties of languages represented in the locally nameless style, a significant set of lemmas about binding structure and substitutions is needed. Such lemmas either need to be manually proved or generated from some language specifications, each time a particular object language is dealt with. We present an approach to deriving those lemmas which can be generically applied to different languages. Our approach is based on Locally Nameless Sets (LNS). It extends the theory of LNS with additional generic operations and axioms on binding structure, from which lemmas about the locally nameless representation can be described and proved without any assumption on the language syntax. Therefore, for any language satisfying the given axioms, which can be proved by straightforward induction, these lemmas are automatically proved. We implement a library for supporting our generic reasoning in Coq with built-in automation and demonstrate its effectiveness by proving equivalence properties of the simply-typed $\lambda$-calculus and the compactness theorem for PCF.