Issue402.agda:12,12-16
x != y of type Unit
when checking that the expression refl has type x == y