  Mechanical proofs by logical relations often involve tedious reasoning about
substitution. In this paper, we show that this is not necessarily the case, by
developing, in Agda, a proof that all simply typed lambda calculus expressions
evaluate to values. A formalization of the proof is remarkably short (~40 lines
of code), making for an excellent introduction to the technique of proofs by
logical relations not only on paper but also in a mechanized setting. We then
show that this process extends to more sophisticated reasoning by also proving
the totality of normalization by evaluation. Although these proofs are not new,
we believe presenting them will empower both new and experienced programming
language theorists in their use of logical relations.
