Issue392.agda:25,11-13
Identifier f2 is declared irrelevant, so it cannot be used here
when checking that the expression f2 has type R1