This paper provides an introduction to the locally nameless approach to the representation of syntax with variable binding, focusing in particular on the use of this technique in formal proofs. First, it explains the benefits of representing bound variables with de Bruijn indices while retaining names for free variables. It then describes the operations involved for manipulating syntax in that form, and shows how to define and reason about judgments on locally nameless terms.