diff --git a/examples/permutations.lp b/examples/permutations.lp
index 8b7eb5a..6f130f4 100644
--- a/examples/permutations.lp
+++ b/examples/permutations.lp
@@ -1,5 +1,5 @@
 #show p/2.
-#external integer(n(0)).
+%#external integer(n(0)).
 
 {p(1..n, 1..n)}.
 
diff --git a/examples/prime.lp b/examples/prime.lp
index a75e0e8..d39a222 100644
--- a/examples/prime.lp
+++ b/examples/prime.lp
@@ -1,5 +1,5 @@
 #show prime/1.
-#external integer(n(0)).
+%#external integer(n(0)).
 
 composite(I * J) :- I = 2..n, J = 2..n.
 prime(N) :- N = 2..n, not composite(N).
diff --git a/examples/schur-numbers.lp b/examples/schur-numbers.lp
index 085205a..fd0fd4f 100644
--- a/examples/schur-numbers.lp
+++ b/examples/schur-numbers.lp
@@ -1,6 +1,6 @@
 #show in/2.
-#external integer(n(0)).
-#external integer(r(0)).
+%#external integer(n(0)).
+%#external integer(r(0)).
 
 {in(1..n, 1..r)}.
 covered(I) :- in(I, S).
diff --git a/include/anthem/Arithmetics.h b/include/anthem/Arithmetics.h
deleted file mode 100644
index 0e465b9..0000000
--- a/include/anthem/Arithmetics.h
+++ /dev/null
@@ -1,263 +0,0 @@
-#ifndef __ANTHEM__ARITHMETICS_H
-#define __ANTHEM__ARITHMETICS_H
-
-#include <anthem/AST.h>
-#include <anthem/Utils.h>
-
-namespace anthem
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// Arithmetics
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct DefaultVariableDomainAccessor
-{
-	Domain operator()(const ast::Variable &variable)
-	{
-		return variable.declaration->domain;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
-EvaluationResult isArithmetic(const ast::Term &term, Arguments &&...);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
-struct IsTermArithmeticVisitor
-{
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::BinaryOperation &binaryOperation, Arguments &&... arguments)
-	{
-		const auto isLeftArithemtic = isArithmetic<VariableDomainAccessor>(binaryOperation.left, std::forward<Arguments>(arguments)...);
-		const auto isRightArithmetic = isArithmetic<VariableDomainAccessor>(binaryOperation.right, std::forward<Arguments>(arguments)...);
-
-		if (isLeftArithemtic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::False || isRightArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Boolean &, Arguments &&...)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Function &function, Arguments &&...)
-	{
-		switch (function.declaration->domain)
-		{
-			case Domain::Noninteger:
-				return EvaluationResult::False;
-			case Domain::Integer:
-				return EvaluationResult::True;
-			case Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Integer &, Arguments &&...)
-	{
-		return EvaluationResult::True;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Interval &interval, Arguments &&... arguments)
-	{
-		const auto isFromArithmetic = isArithmetic<VariableDomainAccessor>(interval.from, std::forward<Arguments>(arguments)...);
-		const auto isToArithmetic = isArithmetic<VariableDomainAccessor>(interval.to, std::forward<Arguments>(arguments)...);
-
-		if (isFromArithmetic == EvaluationResult::Error || isToArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isFromArithmetic == EvaluationResult::False || isToArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (isFromArithmetic == EvaluationResult::Unknown || isToArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::SpecialInteger &, Arguments &&...)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::String &, Arguments &&...)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::UnaryOperation &unaryOperation, Arguments &&... arguments)
-	{
-		const auto isArgumentArithmetic = isArithmetic<VariableDomainAccessor>(unaryOperation.argument, std::forward<Arguments>(arguments)...);
-
-		switch (unaryOperation.operator_)
-		{
-			case ast::UnaryOperation::Operator::Absolute:
-				return (isArgumentArithmetic == EvaluationResult::False ? EvaluationResult::Error : isArgumentArithmetic);
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Variable &variable, Arguments &&... arguments)
-	{
-		const auto domain = VariableDomainAccessor()(variable, std::forward<Arguments>(arguments)...);
-
-		switch (domain)
-		{
-			case Domain::Noninteger:
-				return EvaluationResult::False;
-			case Domain::Integer:
-				return EvaluationResult::True;
-			case Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template <class VariableDomainAccessor, class... Arguments>
-EvaluationResult isArithmetic(const ast::Term &term, Arguments &&... arguments)
-{
-	return term.accept(IsTermArithmeticVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult isInteger(const ast::Term &term);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct IsTermIntegerVisitor
-{
-	static EvaluationResult visit(const ast::BinaryOperation &binaryOperation)
-	{
-		const auto isLeftArithemtic = isArithmetic(binaryOperation.left);
-		const auto isRightArithmetic = isArithmetic(binaryOperation.right);
-
-		if (isLeftArithemtic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::False || isRightArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (binaryOperation.operator_ == ast::BinaryOperation::Operator::Division)
-			return EvaluationResult::False;
-
-		if (isLeftArithemtic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::Boolean &)
-	{
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::Function &function)
-	{
-		switch (function.declaration->domain)
-		{
-			case Domain::Noninteger:
-				return EvaluationResult::False;
-			case Domain::Integer:
-				return EvaluationResult::True;
-			case Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::Integer &)
-	{
-		return EvaluationResult::True;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Interval &)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::SpecialInteger &)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::String &)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::UnaryOperation &unaryOperation)
-	{
-		const auto isArgumentArithmetic = isArithmetic(unaryOperation.argument);
-
-		switch (unaryOperation.operator_)
-		{
-			case ast::UnaryOperation::Operator::Absolute:
-				return (isArgumentArithmetic == EvaluationResult::False ? EvaluationResult::Error : isArgumentArithmetic);
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::Variable &variable)
-	{
-		switch (variable.declaration->domain)
-		{
-			case Domain::Noninteger:
-				return EvaluationResult::False;
-			case Domain::Integer:
-				return EvaluationResult::True;
-			case Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-inline EvaluationResult isInteger(const ast::Term &term)
-{
-	return term.accept(IsTermIntegerVisitor());
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-
-#endif
diff --git a/include/anthem/Type.h b/include/anthem/Type.h
new file mode 100644
index 0000000..8a5870f
--- /dev/null
+++ b/include/anthem/Type.h
@@ -0,0 +1,166 @@
+#ifndef __ANTHEM__ARITHMETICS_H
+#define __ANTHEM__ARITHMETICS_H
+
+#include <anthem/AST.h>
+#include <anthem/Utils.h>
+
+namespace anthem
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Arithmetics
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct DefaultVariableDomainAccessor
+{
+	Domain operator()(const ast::Variable &variable)
+	{
+		return variable.declaration->domain;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
+Type type(const ast::Term &term, Arguments &&...);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
+struct TermTypeVisitor
+{
+	template <class... Arguments>
+	static Type visit(const ast::BinaryOperation &binaryOperation, Arguments &&... arguments)
+	{
+		const auto leftType = type<VariableDomainAccessor>(binaryOperation.left, std::forward<Arguments>(arguments)...);
+		const auto rightType = type<VariableDomainAccessor>(binaryOperation.right, std::forward<Arguments>(arguments)...);
+
+		// Binary operations on empty sets return an empty set (also with division)
+		if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Binary operations on nonintegers return an empty set (also with division)
+		if (leftType.domain == Domain::Noninteger || rightType.domain == Domain::Noninteger)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Binary operations on unknown types return an unknown set
+		if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
+			return {Domain::Unknown, SetSize::Unknown};
+
+		// Divisions return an unknown set
+		if (binaryOperation.operator_ == ast::BinaryOperation::Operator::Division)
+			return {Domain::Integer, SetSize::Unknown};
+
+		// Binary operations on integer sets of unknown size return an integer set of unknown size
+		if (leftType.setSize == SetSize::Unknown || rightType.setSize == SetSize::Unknown)
+			return {Domain::Integer, SetSize::Unknown};
+
+		// Binary operations on integer sets with multiple elements return an integer set with multiple elements
+		if (leftType.setSize == SetSize::Multi || rightType.setSize == SetSize::Multi)
+			return {Domain::Integer, SetSize::Multi};
+
+		// Binary operations on plain integers return a plain integer
+		return {Domain::Integer, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Boolean &, Arguments &&...)
+	{
+		return {Domain::Noninteger, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Function &function, Arguments &&...)
+	{
+		// TODO: check that functions cannot return sets
+
+		return {function.declaration->domain, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Integer &, Arguments &&...)
+	{
+		return {Domain::Integer, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Interval &interval, Arguments &&... arguments)
+	{
+		const auto fromType = type<VariableDomainAccessor>(interval.from, std::forward<Arguments>(arguments)...);
+		const auto toType = type<VariableDomainAccessor>(interval.to, std::forward<Arguments>(arguments)...);
+
+		// Intervals with empty sets return an empty set
+		if (fromType.setSize == SetSize::Empty || toType.setSize == SetSize::Empty)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Intervals with nonintegers return an empty set
+		if (fromType.domain == Domain::Noninteger || toType.domain == Domain::Noninteger)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Intervals with unknown types return an unknown set
+		if (fromType.domain == Domain::Unknown || toType.domain == Domain::Unknown)
+			return {Domain::Unknown, SetSize::Unknown};
+
+		// Intervals with integers generally return integer sets
+		// TODO: handle 1-element intervals such as 1..1 and empty intervals such as 2..1
+		return {Domain::Integer, SetSize::Unknown};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::SpecialInteger &, Arguments &&...)
+	{
+		return {Domain::Noninteger, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::String &, Arguments &&...)
+	{
+		return {Domain::Noninteger, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::UnaryOperation &unaryOperation, Arguments &&... arguments)
+	{
+		assert(unaryOperation.operator_ == ast::UnaryOperation::Operator::Absolute);
+
+		const auto argumentType = type<VariableDomainAccessor>(unaryOperation.argument, std::forward<Arguments>(arguments)...);
+
+		// Absolute value of an empty set returns an empty set
+		if (argumentType.setSize == SetSize::Empty)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Absolute value of nonintegers returns an empty set
+		if (argumentType.domain == Domain::Noninteger)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Absolute value of integers returns the same type
+		if (argumentType.domain == Domain::Integer)
+			return argumentType;
+
+		return {Domain::Unknown, SetSize::Unknown};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Variable &variable, Arguments &&... arguments)
+	{
+		const auto domain = VariableDomainAccessor()(variable, std::forward<Arguments>(arguments)...);
+
+		return {domain, SetSize::Unit};
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class VariableDomainAccessor, class... Arguments>
+Type type(const ast::Term &term, Arguments &&... arguments)
+{
+	return term.accept(TermTypeVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+
+#endif
diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h
index 0a56c2a..cc81102 100644
--- a/include/anthem/Utils.h
+++ b/include/anthem/Utils.h
@@ -52,6 +52,24 @@ enum class Domain
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+enum class SetSize
+{
+	Empty,
+	Unit,
+	Multi,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Type
+{
+	Domain domain{Domain::Unknown};
+	SetSize setSize{SetSize::Unknown};
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 }
 
 #endif
diff --git a/src/anthem/IntegerVariableDetection.cpp b/src/anthem/IntegerVariableDetection.cpp
index fcefc33..450caa9 100644
--- a/src/anthem/IntegerVariableDetection.cpp
+++ b/src/anthem/IntegerVariableDetection.cpp
@@ -1,11 +1,11 @@
 #include <anthem/IntegerVariableDetection.h>
 
-#include <anthem/Arithmetics.h>
 #include <anthem/ASTCopy.h>
 #include <anthem/ASTUtils.h>
 #include <anthem/ASTVisitors.h>
 #include <anthem/Exception.h>
 #include <anthem/Simplification.h>
+#include <anthem/Type.h>
 #include <anthem/Utils.h>
 #include <anthem/output/AST.h>
 
@@ -55,9 +55,9 @@ struct VariableDomainMapAccessor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
+Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
 {
-	return isArithmetic<VariableDomainMapAccessor>(term, variableDomainMap);
+	return type<VariableDomainMapAccessor>(term, variableDomainMap);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -122,19 +122,22 @@ struct EvaluateFormulaVisitor
 
 	static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
 	{
-		const auto isLeftArithmetic = isArithmetic(comparison.left, variableDomainMap);
-		const auto isRightArithmetic = isArithmetic(comparison.right, variableDomainMap);
+		const auto leftType = type(comparison.left, variableDomainMap);
+		const auto rightType = type(comparison.right, variableDomainMap);
 
-		if (isLeftArithmetic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
+		// Comparisons with empty sets always return false
+		if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
+			return EvaluationResult::False;
 
-		if (isLeftArithmetic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
+		// If either side has an unknown domain, the result is unknown
+		if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
 			return EvaluationResult::Unknown;
 
-		if (isLeftArithmetic == isRightArithmetic)
+		// If both sides have the same domain, the result is unknown
+		if (leftType.domain == rightType.domain)
 			return EvaluationResult::Unknown;
 
-		// Handle the case where one side is arithmetic but the other one isn’t
+		// If one side is integer, but the other one isn’t, they are not equal
 		switch (comparison.operator_)
 		{
 			case ast::Comparison::Operator::Equal:
@@ -179,19 +182,25 @@ struct EvaluateFormulaVisitor
 
 	static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
 	{
-		const auto isElementArithmetic = isArithmetic(in.element, variableDomainMap);
-		const auto isSetArithmetic = isArithmetic(in.set, variableDomainMap);
+		const auto elementType = type(in.element, variableDomainMap);
+		const auto setType = type(in.set, variableDomainMap);
 
-		if (isElementArithmetic == EvaluationResult::Error || isSetArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
+		// The element to test shouldn’t be empty or a proper set by itself
+		assert(elementType.setSize != SetSize::Empty && elementType.setSize != SetSize::Multi);
 
-		if (isElementArithmetic == EvaluationResult::Unknown || isSetArithmetic == EvaluationResult::Unknown)
+		// If the set is empty, no element can be selected
+		if (setType.setSize == SetSize::Empty)
+			return EvaluationResult::False;
+
+		// If one of the sides has an unknown type, the result is unknown
+		if (elementType.domain == Domain::Unknown || setType.domain == Domain::Unknown)
 			return EvaluationResult::Unknown;
 
-		if (isElementArithmetic == isSetArithmetic)
+		// If both sides have the same domain, the result is unknown
+		if (elementType.domain == setType.domain)
 			return EvaluationResult::Unknown;
 
-		// If one side is arithmetic, but the other one isn’t, set inclusion is never satisfied
+		// If one side is integer, but the other one isn’t, set inclusion is never satisfied
 		return EvaluationResult::False;
 	}
 
@@ -250,10 +259,10 @@ struct EvaluateFormulaVisitor
 			if (parameter.domain != Domain::Integer)
 				continue;
 
-			const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
+			const auto argumentType = type(argument, variableDomainMap);
 
-			if (isArgumentArithmetic == EvaluationResult::Error || isArgumentArithmetic == EvaluationResult::False)
-				return isArgumentArithmetic;
+			if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
+				return EvaluationResult::Error;
 		}
 
 		return EvaluationResult::Unknown;
@@ -397,15 +406,10 @@ struct CheckIfDefinitionFalseFunctor
 
 		clearVariableDomainMap(variableDomainMap);
 
-		auto result = evaluate(definition, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::False)
-			return OperationResult::Unchanged;
-
 		// As a hypothesis, make the parameter’s domain noninteger
 		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
 
-		result = evaluate(definition, variableDomainMap);
+		const auto result = evaluate(definition, variableDomainMap);
 
 		if (result == EvaluationResult::Error || result == EvaluationResult::False)
 		{
@@ -430,15 +434,10 @@ struct CheckIfQuantifiedFormulaFalseFunctor
 
 		clearVariableDomainMap(variableDomainMap);
 
-		auto result = evaluate(quantifiedFormula, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::False)
-			return OperationResult::Unchanged;
-
 		// As a hypothesis, make the parameter’s domain noninteger
 		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
 
-		result = evaluate(quantifiedFormula, variableDomainMap);
+		const auto result = evaluate(quantifiedFormula, variableDomainMap);
 
 		if (result == EvaluationResult::Error || result == EvaluationResult::False)
 		{
@@ -463,15 +462,10 @@ struct CheckIfCompletedFormulaTrueFunctor
 
 		clearVariableDomainMap(variableDomainMap);
 
-		auto result = evaluate(completedFormula, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::True)
-			return OperationResult::Unchanged;
-
 		// As a hypothesis, make the parameter’s domain noninteger
 		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
 
-		result = evaluate(completedFormula, variableDomainMap);
+		const auto result = evaluate(completedFormula, variableDomainMap);
 
 		if (result == EvaluationResult::Error || result == EvaluationResult::True)
 		{
diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index 3d00eaf..33303fc 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -2,10 +2,10 @@
 
 #include <optional>
 
-#include <anthem/Arithmetics.h>
 #include <anthem/ASTCopy.h>
 #include <anthem/Equality.h>
 #include <anthem/SimplificationVisitors.h>
+#include <anthem/Type.h>
 #include <anthem/output/AST.h>
 
 namespace anthem
@@ -524,11 +524,14 @@ struct SimplificationRuleIntegerSetInclusion
 
 		auto &in = formula.get<ast::In>();
 
-		const auto isElementInteger = isInteger(in.element);
-		const auto isSetInteger = isInteger(in.set);
+		const auto elementType = type(in.element);
+		const auto setType = type(in.set);
 
-		if (isElementInteger != EvaluationResult::True || isSetInteger != EvaluationResult::True)
+		if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
+		    || elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
+		{
 			return OperationResult::Unchanged;
+		}
 
 		formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));