Hi, Marco. You might want to see a similar question that I asked last year and its replies: https://lists.chalmers.se/pipermail/agda/2014/007282.html -- Kenichi Asai