[Agda] simple question

[silvio at cs.ioc.ee]

Hi All,

>> Hello,
>>
>>    I'm trying to follow along in the very good paper "Dependent Types At
>> Work" written by Ana Bove and Peter Dybjer.  I'm stuck at trying to prove
>> "eq-succ", which is one of the exercises in Section 4.4.  The closest I can
>> make it is the following:

CUT

>
> This is probably a stupid question considering I haven't looked at the
> cited work, but what's wrong with just ?cong suc??
>
> --
> Mateusz K.

I agree with Mateusz. This is actually how I did it when I was doing  
the same exercise.

Best regards,

Silvio