Issue998c.agda:5,9-10 A !=< A of type Set (because one is a variable and one a defined identifier) when checking that the expression a has type A