[Agda] no longer type checks

[Martin Escardo]

This

lemma : in₀ x ≡ in₁ y → ⊥
lemma ()

used to compile, where "in" are the injections into X + Y.

Now I get, in 2.3.2,

"The variables
   .X₁
   .Y₁
   x₁
   .X₁
   .Y₁
   y₁
in the indices
   in₀ x₁
   in₁ y₁
are not distinct (note that parameters count as constructor
arguments)
when checking that the clause lemma () has type in₀ x ≡ in₁ y → ⊥"

Is that intended behaviour?

What would be the easiest solution to make this lemma work?

Thanks,
Martin

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe