Issue530.agda:20,1-10
k a != w of type Unit
when checking that the type (w : Unit) → F w p of the generated
with function is well-formed