LevelUnification.agda:12,20-24
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):
  {lsuc a} ≟ {lsuc b}
  {A} ≟ {B}
  x ≟ y
when checking that the pattern refl has type x ≡ y
