Axiom K

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$