Issue1435-helper.agda:28,29-33
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):
  {C (Box A)} ≟ {C (Box B)}
  c₁ A ≟ c₁ B
when checking that the pattern refl has type c₁ A ≅ c₁ B
