SizedTypesRigidVarClash.agda:19,9-14
.i !=< .j of type Size
when checking that the expression suc x has type Nat