[TYPES] Is one-step conversion rule of CC equivalent to the multi-step one?

[Yang, Yanpeng]

Dear all,

The conversion rule of the Calculus of Constructions (CC) is usually
defined as follows:

G |- e : A
G |- A : s
A ==beta B
------------------- Conv
G |- e : B

I wonder if this rule is equivalent to the one using *one-step* beta
reduction:

G |- e : A
G |- A : s
A --> B \/ B --> A
-------------------------- Conv-Step
G |- e : B

This "Conv-Step" rule is shown in Geuvers' paper [1, Definition 4.1] but
which never mentions if it is equivalent to the original "Conv" rule.

So, my question is: has it ever been proved that the two conversion rules
are equivalent? If so, what is the appropriate article to refer to for this
proof?

Thanks a lot!

Sincerely,
Yanpeng

[1] Geuvers, Herman. "A short and flexible proof of Strong Normalization
for the Calculus of Constructions." International Workshop on Types for
Proofs and Programs. Springer, Berlin, Heidelberg, 1994.
URL: http://flint.cs.yale.edu/trifonov/cs629/Geuvers-SN-CC-2up.ps