WithoutK7.agda:14,1-9
The variables
  x₁
which are used (perhaps as constructor parameters) in the index
expressions
  d
are free in the parameters
  x₁
when checking that the clause Foo x () has type
(x : I) → P x d → Set