WithoutK10.agda:12,5-6
The variables
  x
which are used (perhaps as constructor parameters) in the index
expressions
  x
are free in the parameters
  {A}
  (λ {unit → x}) {A} {x}
when checking that the pattern d has type
D {A} ((λ {unit → x}) {A} {x}) x