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