[Agda] simple question

[Andrew Harris]

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:

{- proof of eq-succ -}
eq-succ : {n m : Nat} → n == m → succ n == succ m
eq-succ (refl m) = natrec {(\k → (k + m) == (plus k m))} (refl m) (\i h →
((succ i) + m) == (plus (succ i) m)) m

But this does not typecheck, I get the error:

Set !=< (succ i + m) == plus (succ i) m of type Set₁
when checking that the expression (succ i + m) == plus (succ i) m
has type (succ i + m) == plus (succ i) m

I'm stuck -- I don't quite understand what I'm supposed to create an
element of Set_1 that has a signature of (succ i + m) == plus (succ i) m, (if
that's what I'm supposed to do).  Any hints would be appreciated!

-andrew
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141013/f3c8f3c3/attachment.html