On 31 May 2013 01:19, Andreas Abel <andreas.abel at ifi.lmu.de> wrote: > but the current criterion is too restrictive still. I agree. I reported this issue, http://code.google.com/p/agda/issues/detail?id=865. -- Andrés