A note for any occasion: my programs are stuck under Agda-2.3.2.2 (2.3.2.2 looks too buggy). And Agda of darcs of November 25, 2013 looks all right, so far (apart from various effects which I do not understand, where I need to rewrite a proof in a different style to make it type-checked). Regards, ------ Sergei