[TYPES] Conversion elimination lemma for Pure Type Systems?

[Ahn, Ki Yung]

While I'm trying to prove a property of a calculus which is a variation
of PTS, I needed a conversion elimination lemma for PTS which can be
stated as follows:

"When a PTS typing judgment |- M : A is provable and the term M and its
type A are both in normal forms, then there exists a derivation that
does not use any conversion rule."

Of course, I am assuming the equality in the conversion rule of PTS to
be beta-equality only, since other definitional equality (e.g. s1 = s2
for some sort s1 and s2) can obviously require conversion rule for the
judgments of terms and types with normal forms.

Seems like quite an obvious property, so I am wondering whether there
has there been any proofs for such lemma in the literature?

Thanks in advance.