In the classic the calculus of constructions paper there is a rule that states
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?