Definition isdeceqnat: isdeceq nat. Proof. unfold isdeceq. intro x. induction x as [ | x IHx ]. - intro x'. induction x'. + apply (ii1 (idpath O)). + apply (ii2 (negpaths0sx x')). - intro x'. induction x'. + apply (ii2 (negpathssx0 x)). + induction (IHx x') as [ p | e ]. * apply (ii1 (maponpaths S p)). * apply (ii2 (noeqinjS _ _ e)). Defined.