> Ulf recently changed Agda to reduce the need for workarounds: Thanks for information. For the moment I am happy with my solution - it allows me to do what I need to do and I think it can be easily adjusted in the future once the new stable Agda is released. Janek