Is this $\beta$-reduction well defined?
Beta-reduction is only allowed when the argument does not contain any free variable that is bound in the function. So before you can beta-reduce $(\lambda x. \lambda y.x) y$, you must rename the bound variable $y$ using alpha-conversion.

Formally speaking, beta-reduction and equivalence are defined not over lambda terms, but over lambda terms modulo alpha-conversion. So by performing alpha-conversion, you are not changing the term.

$$
  (\lambda x. \lambda y.x) y =_\alpha (\lambda x. \lambda z.x) y
  \to_\beta \lambda z.y
$$

An alternative approach is to treat terms syntactically, and allow the beta-reduction, but perform the alpha-conversion as part of the substitution. The two approaches can be shown formally to be equivalent (for almost all uses of the lambda calculus, this is an unimportant presentation detail).

$$
  (\lambda x. \lambda y.x) y \to_\beta (\lambda y.x)[x\leftarrow y]
  =_\alpha (\lambda z.x)[x\leftarrow y] = (\lambda x.y)
$$