SizedTypesRigidVarClash.agda:19,1-14 Cannot solve size constraints _size_12 .i .j x ≤ .j .i ≤ _size_12 .i .j x Reason: Inconsistent constraints when checking the definition of inc