Martin-Löf Extensional Type theory differs from its intensional counterpart in that it contains the so-called *reflection rule* that says that if $p : x = y$, then actually $x \equiv y$ (i.e. $x$ and $y$ are definitionally or judgementally equivalent). Its known that this causes strong normalization to fail and type-checking to be undecidable.

More to the point, it is known that it also trivializes higher paths in a type in the sense that for any $p, q: x = y$, $p \equiv q$. I wonder why is this so?

I heard this is because it implies that for any $p : x = x$, $p \equiv refl_x$. But I can't see why this is true. As far I can see, given any such $p$ the reflection rule only implies that $x \equiv x$, which is true anyway, since each term is definitionally equal to itself - with or without the rule. So how come we conclude that $p \equiv refl_x$? What am I missing?

Thanks!