<div dir="ltr"><div><div><div>Hello,<br><br></div>   I&#39;m trying to follow along in the very good paper &quot;Dependent Types At Work&quot; written by Ana Bove and Peter Dybjer.  I&#39;m stuck at trying to prove &quot;eq-succ&quot;, which is one of the exercises in Section 4.4.  The closest I can make it is the following:<br><br><span style="font-family:courier new,monospace">{- proof of eq-succ -}<br>eq-succ : {n m : Nat} â†’ n == m â†’ succ n == succ m<br>eq-succ (refl m) = natrec {(\k â†’ (k + m) == (plus k m))} (refl m) (\i h â†’ ((succ i) + m) == (plus (succ i) m)) m<br><br></span></div><span style="font-family:courier new,monospace"><font face="arial,helvetica,sans-serif">But this does not typecheck</font>, I get the error:<br><br>Set !=&lt; (succ i + m) == plus (succ i) m of type Set₁<br>when checking that the expression (succ i + m) == plus (succ i) m<br>has type (succ i + m) == plus (succ i) m<br><br></span></div><span style="font-family:courier new,monospace"><font face="arial,helvetica,sans-serif">I&#39;m stuck -- I don&#39;t quite understand what I&#39;m supposed to create an element of Set_1 that has a signature of </font></span><span style="font-family:courier new,monospace">(succ i + m) == plus (succ i) m, <span style="font-family:arial,helvetica,sans-serif">(if that&#39;s what I&#39;m supposed to do).  Any hints would be appreciated!</span><br></span><div><div><div><br></div><div>-andrew<br></div></div></div></div>