WithoutK4.agda:10,16-20
The indices
  f y
are not constructors (or literals) applied to variables (note that
parameters count as constructor arguments)
when checking that the pattern refl has type x ≡ f y