# Typo in the calculus of constructions paper?

In the classic the calculus of constructions paper there is a rule that states

(page 7 of the pdf, page 101 of the original document)

This rule would mean that any context is reducible to a member of that context. This seems like it shouldn't be correct, as it would entail

1 ≅ Nat
3 ≅ Nat
1 ≅ 3


if Nat is a context.

I think the best interpretation is that the lower delta was meant to be an M. Especially considering the rules given on the next page.

So is this simply a typo, or some subtle logical rule that I don't understand?

You are correct, there is an error in that paper, and the rule should indeed read: $$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M}$$
the use of jugements of this style for equality (sometimes called "typed equality") originates already in Martin-Löf, I think (see here for example). It's often replaced with an untyped operational definition in modern treatments, where there is no jugement of the form $\Gamma\vdash N\cong M$, and conversion is defined on raw terms.