Stefani and coauthors, in various papers, have advocated the usefulness of constructs for localities and passivation in higher-order process languages. They have also shown that the constructs may have surprising consequences on the theory of the languages. In this paper, dedicated to Jean-Bernard Stefani, we show that, in contrast, proof techniques based on unique-solution of equations are robust enough to bear the presence of such constructs.