[Agda] `reasoninig' example

[Serge D. Mechveliani]

Dear all,
I have a beginner question about using the `reasoning' parts of the
standard library lib-0.7. 

The attachement              t.agda.zip  

contains a 10 line code for  uniqueIverse  in a monoid  which uses  
                             unityLaw, cong, sym, refl, trans, assoc. 

Can anybody demonstrate, please, how can this be (approximately) rewritten 
by using EqReasoning, or may be, some other `reasoning' part of the 
library?

Thanks,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: t.agda.zip
Type: application/zip
Size: 530 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130224/5cc71a10/t.agda.zip