  We study proof techniques for bisimilarity based on unique solution of
equations. We draw inspiration from a result by Roscoe in the denotational
setting of CSP and for failure semantics, essentially stating that an equation
(or a system of equations) whose infinite unfolding never produces a divergence
has the unique-solution property. We transport this result onto the operational
setting of CCS and for bisimilarity. We then exploit the operational approach
to: refine the theorem, distinguishing between different forms of divergence;
derive an abstract formulation of the theorems, on generic LTSs; adapt the
theorems to other equivalences such as trace equivalence, and to preorders such
as trace inclusion. We compare the resulting techniques to enhancements of the
bisimulation proof method (the `up-to techniques'). Finally, we study the
theorems in name-passing calculi such as the asynchronous $\pi$-calculus, and
use them to revisit the completeness part of the proof of full abstraction of
Milner's encoding of the $\lambda$-calculus into the $\pi$-calculus for
L\'evy-Longo Trees.
