[Agda] predicate for sub-type

[Serge D. Mechveliani]

пPeople,
I have a beginner question about using a predicate to define a subset.
One variant does type-check, and a `nicer' one does not.
The program (quite small and simple) and questions are  attached  to this 
letter as 
          Main.agda.zip 

(because I hope that this way I send the math symbols as they are).

Thanks,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.agda.zip
Type: application/zip
Size: 1324 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130203/c61bb2c7/Main.agda.zip