ShapeIrrelevantIndex.agda:13,22-23
Variable n is declared irrelevant, so it cannot be used here
when checking that the expression n has type Nat