  The "Harmony Lemma", as formulated by Sangiorgi & Walker, establishes the
equivalence between the labelled transition semantics and the reduction
semantics in the $\pi$-calculus. Despite being a widely known and accepted
result for the standard $\pi$-calculus, this assertion has never been
rigorously proven, formally or informally. Hence, its validity may not be
immediately apparent when considering extensions of the $\pi$-calculus.
Contributing to the second challenge of the Concurrent Calculi Formalization
Benchmark -- a set of challenges tackling the main issues related to the
mechanization of concurrent systems -- we present a formalization of this
result for the fragment of the $\pi$-calculus examined in the Benchmark. Our
formalization is implemented in Beluga and draws inspiration from the HOAS
formalization of the LTS semantics popularized by Honsell et al. In passing, we
introduce a couple of useful encoding techniques for handling telescopes and
lexicographic induction.
