[Agda] EqReasoning example

[Serge D. Mechveliani]

On Mon, Mar 04, 2013 at 06:24:38PM +0100, Andreas Abel wrote:
> Hello Sergei,
> 
> you are simply using the wrong identifier for the equality chaining.
> The correct one is
> 
>   \equiv\<      \>
> 
> and you used s.th. like
> 
>   \approx( ... )
> 
> First, parentheses () cannot be part of an identifier, since they
> are special symbols in Agda (and any language I know).


Great! It works.
I must have recalled my adventure with  \equiv\< $ \>.
My emacs graphics shows very closely the above two kinds of parenthesis.
I rename the chaining one to  \equiv[ ],  so that it is graphically 
visible now.

Thanks,

------
Sergei