Successor of integers in System F In Girard, Proofs and Types, the operator successor is defined as follows:
$St\equiv\Lambda X.\lambda x:X \lambda y:X\to X.y(tXxy)$, while 
$0\equiv\Lambda X.\lambda x:X \lambda y:X\to X.x$.
If I try to compute $S0$, I get (using $\alpha$-reduction even if it might not be necessary):
$\S0\equiv\Lambda X.\lambda x:X \lambda y:X\to X(\Lambda U.\lambda u:U\lambda v:U\to U.uXxy)$
$\to_\beta\Lambda X.\lambda x:X\lambda y:X\to X.y(\lambda u:X\lambda v:X\to X.u(xy))$
$\to_\beta\Lambda X.\lambda x:X\lambda y:X\to X.y(\lambda v:X\to X.xy)$ and now I cannot substitute since $y$ is free in the latter term; even in I apply a new $\alpha$-conversion the result won't look as a numeral at all.
If I try the same procedure, without use of the conversion, I get as a result
$\Lambda X.\lambda x:X\lambda y:X\to X.xy$, which is nicer but still wrong. Now, where am I making mistakes and which one of the approch should I use? I think I sould start with $\alpha$-conversion, as, in principle, the variables $x,y$ are referred to $S$ and not to $0$., but this computation leads me to a very confusing output.
Since I was asked in the comment to clarify notations and unfortunately I did not found many discussions regarding system F:
$\Lambda$ is the symbol of universal abstraction, $\lambda$ is the symbol for terms abstraction, capital letters rapresent types, while small ones are term variables. Writing $x:X$ I mean the term $x$ inhabitates the type $X$.
 A: Your calculations are wrong.  In fact, they just don't make any sense.  Your initial expansion of $S0$ doesn't match the definition, and then you seem to be "reducing" things when your terms have no $\beta$ redexes.  $\alpha$-conversion correctly applied never changes the normal form, so it would never lead you to get different answers. Note $tXxy$ means $((tX)x)y$. $\beta$-reduction is $(\lambda x:X.E)y \to E[x\mapsto y]$ where $E[x\mapsto y]$ means $E$ with all occurrences of $x$ replaced with $y$ in a capture-avoiding way.  Similarly for $\Lambda$. Also, while they are often omitted, compound terms are implicitly wrapped in parentheses. So $0 \equiv (\Lambda X.\lambda x:X.\lambda y:X\to X.x)$ or to be completely explicit $(\Lambda X.(\lambda x:X.(\lambda y:(X\to X).u)))$. Your expansion of $S0$ may be a mixture of a typo and failing to include parentheses.
The Church-numeral for the natural number $n$ is the $\lambda$-term of the form $$\Lambda N.\lambda z:N.\lambda s:N\to N.s^n z$$ where $s^n z$ is shorthand for for $s$ applied to $z$ $n$-times, e.g. $s^3z = s(s(sz))$. $s^0 z = z$ and so you can verify that the $\lambda$-term for $0$ is indeed the Church-numeral for the number $0$.
The calculation proceeds as follows, note that in this case at every point there is only one possible $\beta$-redex:
$$\begin{align}
S0 & \equiv \Lambda X.\lambda x : X.\lambda y:X\to X.y(0Xxy) & \text{by definition of }S \\
& \equiv \Lambda X.\lambda x : X.\lambda y:X\to X.y((\Lambda U.\lambda u:U.\lambda v:U\to U.u)Xxy) & \text{by definition of 0 and }\alpha \\
& \to \Lambda X.\lambda x : X.\lambda y:X\to X.y((\lambda u:X.\lambda v:X\to X.u)xy) & \beta\text{ reduction} \\
& \to \Lambda X.\lambda x : X.\lambda y:X\to X.y((\lambda v:X\to X.x)y) & \beta\text{ reduction} \\
& \to \Lambda X.\lambda x : X.\lambda y:X\to X.yx & \beta\text{ reduction} \\
\end{align}$$
This is its normal form.  Further, it is $\alpha$-equivalent to the Church-numeral for $1$.
