Nominal unification: How this lemma is proved?
chi's answer is mostly correct, but I've poured through the paper, and can probably fill in the gaps a bit:

The proof proceeds in 3 steps:


Show that it suffices to prove:
$$\nabla\vdash \sigma(\pi^{-1}.t) \approx \sigma(X) $$
Show that the above derivation is implied by
$$\nabla\vdash \sigma(t)\approx\pi.\sigma(X) $$
Show that in turn this is implied by the assumptions of the theorem.


The structure of the proof is a bit confusing, since it proceeds "backwards", from the conclusion of the theorem to the hypothesis.

The first step involves mostly unpacking the definition of substitutions and the notation $\sigma\ \circ\ [X:=t]$.

The second step is handled by lemmas in the paper (lemmas 2.14 and 2.12 if we're reading the same version). This step is the most complex of the proof.

The last part is performed by changing $\nabla\vdash \sigma(t)\approx\pi.\sigma(X)$ to $\nabla\vdash \pi.\sigma(X)\approx\sigma(t)$ by applying symmetry and once again applying using lemma 2.14 to move $\pi$ "inside" the permutation to get
$$\nabla\vdash \sigma(\pi.X)\approx\sigma(t) $$

which is exactly the assumption!

Again, the only real difficulty is that the proof is working backwards, starting from the conclusion and finding stronger and stronger statements until you get the hypothesis.