G. Allais

The canonical solution is to use a bit of `sed` to drop numbers in the output

For instance: https://github.com/idris-lang/Idris2/blob/main/tests/idris2/basic044/run

> Would this constitute a breaking change? Given that we don't have subtyping for functions whose domain is irrelevant (the following is rejected: ```agda app : {A B : Set}...

[*\*déjà vu\**](https://lists.chalmers.se/pipermail/agda/2016/008657.html)

This was included as part of #32. Thank you and sorry it took so long!