OccursCheck.agda:13,3-7 n != suc n of type Nat when checking that the pattern refl has type n == suc n