[proofplan] The argument converts the reflexivity proof at $a$ into a proof whose second endpoint is $b$. Identity introduction first gives $\operatorname{refl}_a$ as an inhabitant of $\operatorname{Id}_A(a,a)$. Since $a$ and $b$ are definitionally equal terms of type $A$, congruence for the identity type former gives a definitional equality of types $\operatorname{Id}_A(a,a) \equiv \operatorname{Id}_A(a,b)$. The conversion rule then retypes the same term $\operatorname{refl}_a$ at the definitionally equal target type. [/proofplan] [step:Extract the well-formed judgments from the definitional equality hypothesis] Assume $\Gamma \vdash a \equiv b : A$. By the standard well-formedness convention for a judgmental equality of terms, this judgment includes the derivability of $\Gamma \vdash A\ \mathsf{type}$, together with the endpoint typing judgments $\Gamma \vdash a : A$ and $\Gamma \vdash b : A$. These are precisely the formation hypotheses needed to form both identity types $\operatorname{Id}_A(a,a)$ and $\operatorname{Id}_A(a,b)$ in context $\Gamma$. [/step] [step:Introduce reflexivity at the first endpoint] Since $\Gamma \vdash A\ \mathsf{type}$ and $\Gamma \vdash a:A$, the identity type introduction rule gives \begin{align*} \Gamma \vdash \operatorname{refl}_a : \operatorname{Id}_A(a,a). \end{align*} [guided] We now use only the introduction rule for identity types. The rule says that whenever a term $a$ has type $A$ in a context $\Gamma$, there is a reflexivity term witnessing identity of $a$ with itself: \begin{align*} \Gamma \vdash \operatorname{refl}_a : \operatorname{Id}_A(a,a). \end{align*} The required hypothesis for this rule is exactly $\Gamma \vdash a:A$, and this was obtained from the well-formedness of the assumed definitional equality judgment \begin{align*} \Gamma \vdash a \equiv b : A. \end{align*} At this point the second endpoint is still $a$, not $b$. The rest of the proof changes only the type of this already constructed term; it does not construct a new identity proof by identity elimination. [/guided] [/step] [step:Use congruence of the identity type former to identify the two target types] By the congruence hypothesis for the identity type former, the identity type former is congruent in its endpoint arguments under definitional equality. Applying this congruence to the definitional equality $\Gamma \vdash a \equiv b : A$ while keeping the first endpoint fixed at $a$, we obtain the definitional equality of types $\Gamma \vdash \operatorname{Id}_A(a,a) \equiv \operatorname{Id}_A(a,b)\ \mathsf{type}$. The formation judgments from the first step ensure that both sides are well-formed types in the same context $\Gamma$. [/step] [step:Apply conversion to retype the reflexivity term] We have derived $\Gamma \vdash \operatorname{refl}_a : \operatorname{Id}_A(a,a)$ and $\Gamma \vdash \operatorname{Id}_A(a,a) \equiv \operatorname{Id}_A(a,b)\ \mathsf{type}$. By the conversion rule assumed in the theorem statement, applied with the term $\operatorname{refl}_a$, source type $\operatorname{Id}_A(a,a)$, and target type $\operatorname{Id}_A(a,b)$, we conclude $\Gamma \vdash \operatorname{refl}_a : \operatorname{Id}_A(a,b)$. This is the desired judgment. [/step]