Issue1611.agda:15,7-9
I'm not sure if there should be a case for the constructor dt,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  true ≟ _9
when checking that the pattern dt has type D _9
