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$.