y in x = y must be a free variable as it is quantified in B : (y : A) → x ≡ y → Set b for this reasin it can not be specialize to x when doing an induction. So if you want to prove sth for equality, you must first prove sth for x = y to deduce it for x = x, which is not possible for UIP / axiom K.