IrrelevantLevelHurkens.agda:12,31-32
Variable i is declared irrelevant, so it cannot be used here
when checking that the expression i has type Level