WithoutK9.agda:17,26-30
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):
  E.refl ≟ E.refl
Possible reasons why unification failed:
  Cannot apply injectivity to the equation E.refl = E.refl of type
  _≡_ {A} y y because I cannot generalize over the indices [y].
  Cannot eliminate reflexive equation E.refl = E.refl of type
  _≡_ {A} y y because K has been disabled.
when checking that the pattern refl has type
_≡_ {_≡_ {A} y y} E.refl E.refl
