  In a small-step semantics with a deterministic reduction strategy, refocusing
is a transformation that connects a reduction-based normalization function
(i.e., a normalization function that enumerates the successive terms in a
reduction sequence -- the successive reducts) and a reduction-free
normalization function (i.e., a normalization function that does not construct
any reduct because all the reducts are deforested). This transformation was
introduced by Nielsen and the author in the early 2000's with an informal
correctness proof. Since then, it has been used in a variety of settings,
starting with Biernacka and the author's syntactic correspondence between
calculi and abstract machines, and several formal proofs of it have been put
forward. This article presents a simple, if overdue, formal proof of refocusing
that uses the Coq Proof Assistant and is aligned with the simplicity of the
original idea.
