Definitional equality of two propositions about propositional equality

Question

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.3) that:

It is important that definition equality is pervasive so if M and N are definitionally equal then P(M) is definitionally equal to P(N) whatever P is. In particular the proposition stating that M is propositionally equal to N is definitionally equal to the proposition that M is propositionally equal to itself.

What I don't get is how a proposition about equality of M and N propositionally can be definitionally equal to the proposition about propositional equality of M and M ?