Rendering of type-level computation
In your reference [2], Barendregt shows that the rule

$$ \frac{\Gamma\vdash N:\alpha\quad M\rightarrow^* N\quad \alpha\equiv \beta}{\Gamma\vdash N:\beta} $$

is indeed admissible for Pure Type Systems, as (a trivial consequence of) Corollary 5.2.16.

However there is an issue with your original rule already: the rule should read

$$ \frac{\Gamma\vdash N:\alpha\quad\alpha\equiv \beta\quad {\bf \Gamma\vdash\beta : s}}{\Gamma\vdash N:\beta} $$
for some sort $s$, otherwise you may introduce ill-formed types into your typing judgement, like $(\lambda x y. y)\ \Omega\ (\alpha\rightarrow\alpha)$.

This can be a problem for your extended rule, as usually you only allow well-formed types into your context, with a rule along the lines of

$$ \frac{\Gamma\vdash \alpha:s}{\Gamma,x:\alpha\ \ \mathrm{wf}}$$

If you add the relevant well-formedness requirements ($\Delta\ \mathrm{wf}$ and $\Delta\vdash\beta:s$), and restrict the term level to reduction rather than conversion, then your sophisticated rule becomes admissible.

This is a not completely trivial induction, using the following Lemma:


  If $\Gamma\vdash t:\alpha$, $\Gamma\equiv\Delta$ and $\Delta\ \mathrm{wf}$ then $\Gamma\vdash t:\alpha$


The lemma is proven by induction using an application of the conversion rule at the variable case. The theorem is then proven using the above lemma to discharge the conversion case.



You could adopt the opposite point of view of keeping your more general conversion rule and weakening the context formation rule to

$$ \frac{\Gamma\vdash \beta:s\quad \beta\equiv \alpha}{\Gamma,x:\alpha\ \ \mathrm{wf}}$$

then you get a system with possibly ill-formed types, but no additional typeable terms, though I think this is a very non-trivial result.