Uniqueness of Identity Proofs

Definition

Let $T$ be a type theory. The inclusion of axiom $K$ states the following. Let $\Gamma$ be a context, $A$ be a type, and $x,y$ be terms such that, $\Gamma ⊢x,y:A$ Then $K$ states that $\Gamma ;y,y:A;p,q:x{=}_{A}y⊢p{=}_{x=y}q$