IllegalUseOfIrrelevantDeclaration.agda:17,23-33
Identifier irrelevant is declared irrelevant, so it cannot be used
here
when checking that the expression irrelevant p has type
.P (Subset.elem (a # _))