[Agda] EqReasoning example

[Serge D. Mechveliani]

On Tue, Mar 05, 2013 at 01:01:46AM +0400, Serge D. Mechveliani wrote:
> 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\< $ \>.


Correction:  it was  _\<$\>_  (related to the \Pi class).

------
Sergei