Issue2679b.agda:19,10-20
I'm not sure if there should be a case for the constructor conC,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  conB bl br ≟ _17 (a = a) (b = b)
when checking that the pattern conC tl tr has type
C a (_17 (a = a) (b = b))
