[Agda] Preserves-by-2-of-3

[Serge D. Mechveliani]

People,

I define the property  cong-foo  for the function 
                                 foo : (x y : C) -> \neg (y \~~ e) -> C

This means:  "foo  preserves _\~~_, with ignoring the third argument".
And try to set the signature for  cong-foo  by applying a construct 
similar to  _Preserves_2_->_->...  of the Library.

The attached        t.agda.zip 

is the precise code (about 15 lines of the proper code).
I wonder: how to fix it in order to satisfy the type checker?

Thank you in advance for explanation,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: t.agda.zip
Type: application/zip
Size: 1046 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130408/27d0aac1/t.agda.zip