[Agda] explicit irrelevance question

[Darius Jahandarie]

On Sun, Oct 19, 2014 at 5:39 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Sergei, I managed to finish your proof using irrel-f (see below).

{! agda at lists.chalmers.se !}

C-c C-a

-- 
Darius Jahandarie