Why is alpha-equivalence in untyped $\lambda$-calculus substitutive? This is something all introductory texts seem to avoid proving, and many even avoid stating.
We consider untyped $\lambda$-terms on some countably infinite alphabet. If $x$ is a variable and $p$ is an $\alpha$-equivalence class of a term, then we define an $\alpha$-equivalence class $p\left[s/x\right]$ as follows:
begin definition of $\left[s/x\right]$
Let $t$ be a term such that $p=\overline{t}$ (where $\overline{t}$ means the $\alpha$-equivalence class of $t$).
If $t=x$, set $p\left[s/x\right] = \overline{s}$.
If $t=y$ for a variable $y\neq x$, set $p\left[s/x\right] = \overline{y}$.
If $t=t_1t_2$ for two terms $t_1$ and $t_2$, set $p\left[s/x\right] = \overline{\rho\left(t_1\left[s/x\right]\right) \rho\left(t_2\left[s/x\right]\right)}$. Here, $\rho\left(u\right)$ means any representative of the $\alpha$-equivalence class $u$.
If $t=\lambda yr$ for some variable $y\neq x$ and term $r$, and if $y$ appears as a free variable in $s$, set $p\left[s/x\right] = \overline{\lambda y^{\prime}.\rho\left(r\left[y^{\prime}/y\right]\left[s/x\right]\right)}$, where $y^{\prime}$ is some fresh (unused) variable.
If $t=\lambda yr$ for some variable $y\neq x$ and term $r$, and if $y$ does not appear as a free variable in $s$, set $p\left[s/x\right] = \overline{\lambda y .\rho\left(r\left[s/x\right]\right)}$.
If $t=\lambda xr$ for some term $r$, set $p\left[s/x\right] = \overline{\lambda x.\rho\left(r\right)}$.
end definition of $\left[s/x\right]$
How can I prove that this definition makes sense? I. e., that the result never depends on the choice of representatives and on the choice of the free variable $\rho^{\prime}$ ? I know that people like to call things like these intuitively obvious, but to me the definition looks much too complex to speak of triviality. It is like claiming that a code does what one expects it to - it is trivial until one finds the first bug. I have tried the usual structural induction, but I got lost in the casebash (there are much more cases than usually, and one has to prove lemmata about substitution). Is there a readable proof anywhere?
 A: I think this is proved in H. B. Curry and R. Feys. Combinatory Logic, Volume I. North-Holland Co., Amsterdam, Theorem 2a on page 95. The proof, with all the auxiliary results and some consequences, occupies pages 96-103.
A: This is addresses, for example, in A. Gordon and T. Melham's "Five Axioms of Alpha-Conversion". The use de Bruijn indices to get things done. If you can read Slovene, a student of mine has worked out all the nasty details directly in syntax.
A: For the sake of completeness, here is an answer using freely avaliable (online) sources:
Most of this question is actually answered in the first two sections of Chapter 1 of
Jean-Louis Krivine, Lambda-calculus, types and models, 22 January 2009.
http://www.pps.jussieu.fr/~krivine/articles/Lambda.pdf . (This is a very good text, once you have accustomed to the suboptimal formatting.)
What little remains to be done is done at http://www.cip.ifi.lmu.de/~grinberg/mo65420.pdf . This PDF uses the notations of Krivine, but the last six lemmata (Lemmata 1.J-1.O) show that his definition of substitution is equivalent to mine, and that mine is actually well-defined.
A: Actually this is proved in Krivine:

Consider terms $t, t_1, \ldots, t_k \in \Lambda$ and distinct variables
  $x_1, \ldots, x_k$. Then the term $t \left [t_1/x_1, \ldots, t_k/x_k \right] \in \Lambda$ (being the result of the
  replacement of every free occurrence
  of $x_i$ in $t$ by $t_i$, for $i = 1,\ldots, k$) is defined as follows: let
  $\underline{t}, \underline{t}_1,\ldots, \underline{t}_k$ be terms of
  $L$, the equivalence classes of which
  are respectively $t, t_1, \ldots,t_k$. By lemma 1.11, we may assume
  that no bound variable of
  $\underline{t}$ is free in $t_1,\ldots, t_k$. Then $t \left[t_1/x_1,\ldots, t_k/x_k \right]$ is defined as the
  equivalence class of $\underline{t}\left\langle \underline{t}_1/x_1, \ldots,\underline{t}_k/x_k \right\rangle $. Indeed, by
  proposition 1.7, this equivalence
  class does not depend on the choice of
  $\underline{t}, \underline{t}_1,\ldots, \underline{t}_k$.
So the substitution operation $t, t_1,\ldots, t_k \mapsto t \left[ t_1/x_1,\ldots, t_k/x_k \right]$ is well defined in
  $\Lambda$.

The full book, including proposition 1.7 is available at the link above.
