WithoutK3.agda:25,9-13
I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  {A} ≟ {A}
  x ≟ y
Possible reason why unification failed:
  Cannot eliminate reflexive equation A = A of type Set because K has
  been disabled.
when checking that the pattern refl has type _≅_ {A} x {A} y
