Roughly, the strong normalization property for Martin-Löf Intensional Type Theory (MITT) tells us that every closed term $t$ of type $M$ will eventually reach a canonical normal form $t’$ such that it a direct instance of the constructors of $M$.

Now let $A : Type$ with $a,b : A$. If my understanding is correct, for identity type, this means that all closed terms of some $a=b$, are of the form $refl ...$. I would like to better understand how such reduction happens in practice, so let me give you a toy example.

Consider $A, B : Type$ and $w : A \times B$. Thus, we have the type $$ w = (\text{pr1 } w, \text{pr2 } w) $$ and any closed term of it should be reducible to a normal form.

We want to construct explicitly such a closed term $t : w = (\text{pr1 } w, \text{pr2 } w)$, which we do by $$t := \text{prod_induction_principle } w \text{ } (λ a \text{ } b, (refl (a,b))) $$ But now how can we show that $t$ reduces to some term of the form $refl …$ ?