Issue1982.agda:29,19-23
I'm not sure if there should be a case for the constructor up,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  {_} ≟ {_}
  (! t) ∶ (t ∶ A) ≟ A₁
when checking that the pattern up j has type True Γ A
