diff --git a/src/translate/common.rs b/src/translate/common.rs
index eae009f..af328ab 100644
--- a/src/translate/common.rs
+++ b/src/translate/common.rs
@@ -27,12 +27,8 @@ impl FindOrCreateFunctionDeclaration for foliage::FunctionDeclarations
 			Some(value) => std::rc::Rc::clone(value),
 			None =>
 			{
-				let declaration = foliage::FunctionDeclaration
-				{
-					name: name.to_owned(),
-					arity,
-				};
-				let declaration = std::rc::Rc::new(declaration);
+				let declaration = std::rc::Rc::new(foliage::FunctionDeclaration::new(
+					name.to_string(), arity));
 
 				self.insert(std::rc::Rc::clone(&declaration));
 
@@ -55,12 +51,8 @@ impl FindOrCreatePredicateDeclaration for foliage::PredicateDeclarations
 			Some(value) => std::rc::Rc::clone(value),
 			None =>
 			{
-				let declaration = foliage::PredicateDeclaration
-				{
-					name: name.to_owned(),
-					arity,
-				};
-				let declaration = std::rc::Rc::new(declaration);
+				let declaration = std::rc::Rc::new(foliage::PredicateDeclaration::new(
+					name.to_string(), arity));
 
 				self.insert(std::rc::Rc::clone(&declaration));
 
@@ -80,14 +72,10 @@ impl FindOrCreateVariableDeclaration for foliage::VariableDeclarationStack
 		// TODO: check correctness
 		if name == "_"
 		{
-			let variable_declaration = foliage::VariableDeclaration
-			{
-				name: "_".to_owned(),
-			};
-			let variable_declaration = std::rc::Rc::new(variable_declaration);
+			let variable_declaration = std::rc::Rc::new(foliage::VariableDeclaration::new(
+				"_".to_owned()));
 
-			self.free_variable_declarations.insert(
-				std::rc::Rc::clone(&variable_declaration));
+			self.free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration));
 
 			return variable_declaration;
 		}
@@ -106,17 +94,17 @@ pub(crate) fn translate_binary_operator(binary_operator: clingo::ast::BinaryOper
 		| clingo::ast::BinaryOperator::Xor
 			=> return Err(crate::Error::new_unsupported_language_feature("binary logical operators")),
 		clingo::ast::BinaryOperator::Plus
-			=> Ok(foliage::BinaryOperator::Addition),
+			=> Ok(foliage::BinaryOperator::Add),
 		clingo::ast::BinaryOperator::Minus
-			=> Ok(foliage::BinaryOperator::Subtraction),
+			=> Ok(foliage::BinaryOperator::Subtract),
 		clingo::ast::BinaryOperator::Multiplication
-			=> Ok(foliage::BinaryOperator::Multiplication),
+			=> Ok(foliage::BinaryOperator::Multiply),
 		clingo::ast::BinaryOperator::Division
-			=> Ok(foliage::BinaryOperator::Division),
+			=> Ok(foliage::BinaryOperator::Divide),
 		clingo::ast::BinaryOperator::Modulo
 			=> Ok(foliage::BinaryOperator::Modulo),
 		clingo::ast::BinaryOperator::Power
-			=> Ok(foliage::BinaryOperator::Exponentiation),
+			=> Ok(foliage::BinaryOperator::Exponentiate),
 	}
 }
 
@@ -142,25 +130,17 @@ pub(crate) fn translate_comparison_operator(comparison_operator: clingo::ast::Co
 
 pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
 	variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-	-> foliage::Comparison
+	-> foliage::Formula
 {
-	let variable = foliage::Variable
-	{
-		declaration: std::rc::Rc::clone(variable_declaration),
-	};
+	let variable = foliage::Term::variable(variable_declaration);
 
-	foliage::Comparison
-	{
-		operator: foliage::ComparisonOperator::Equal,
-		left: Box::new(foliage::Term::Variable(variable)),
-		right: term,
-	}
+	foliage::Formula::equal(Box::new(variable), term)
 }
 
 pub(crate) fn choose_value_in_term(term: &clingo::ast::Term,
 	variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>,
-	function_declarations: &mut foliage::FunctionDeclarations,
-	variable_declaration_stack: &mut foliage::VariableDeclarationStack)
+	mut function_declarations: &mut foliage::FunctionDeclarations,
+	mut variable_declaration_stack: &mut foliage::VariableDeclarationStack)
 	-> Result<foliage::Formula, crate::Error>
 {
 	match term.term_type()
@@ -168,21 +148,19 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term,
 		clingo::ast::TermType::Symbol(symbol) => match symbol.symbol_type()
 			.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
 		{
-			clingo::SymbolType::Number => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
-				Box::new(foliage::Term::Integer(symbol.number()
+			clingo::SymbolType::Number => Ok(choose_value_in_primitive(
+				Box::new(foliage::Term::integer(symbol.number()
 					.map_err(|error| crate::Error::new_logic("clingo error").with(error))?)),
-				variable_declaration))),
-			clingo::SymbolType::Infimum => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
-				Box::new(foliage::Term::SpecialInteger(foliage::SpecialInteger::Infimum)),
-				variable_declaration))),
-			clingo::SymbolType::Supremum => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
-				Box::new(foliage::Term::SpecialInteger(foliage::SpecialInteger::Supremum)),
-				variable_declaration))),
-			clingo::SymbolType::String => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
-				Box::new(foliage::Term::String(symbol.string()
+				variable_declaration)),
+			clingo::SymbolType::Infimum => Ok(choose_value_in_primitive(
+				Box::new(foliage::Term::infimum()), variable_declaration)),
+			clingo::SymbolType::Supremum => Ok(choose_value_in_primitive(
+				Box::new(foliage::Term::supremum()), variable_declaration)),
+			clingo::SymbolType::String => Ok(choose_value_in_primitive(
+				Box::new(foliage::Term::string(symbol.string()
 					.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
 					.to_string())),
-				variable_declaration))),
+				variable_declaration)),
 			clingo::SymbolType::Function =>
 			{
 				let arguments = symbol.arguments()
@@ -199,28 +177,195 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term,
 					.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
 
 				let constant_declaration = function_declarations.find_or_create(constant_name, 0);
+				let function = foliage::Term::function(&constant_declaration, vec![]);
 
-				let function = foliage::Term::Function(foliage::Function
-				{
-					declaration: constant_declaration,
-					arguments: vec![],
-				});
-
-				Ok(foliage::Formula::Comparison(choose_value_in_primitive(Box::new(function), variable_declaration)))
+				Ok(choose_value_in_primitive(Box::new(function), variable_declaration))
 			}
 		},
 		clingo::ast::TermType::Variable(variable_name) =>
 		{
 			let other_variable_declaration = variable_declaration_stack.find_or_create(variable_name);
+			let other_variable = foliage::Term::variable(&other_variable_declaration);
 
-			let other_variable = foliage::Term::Variable(foliage::Variable
-			{
-				declaration: other_variable_declaration,
-			});
-
-			Ok(foliage::Formula::Comparison(choose_value_in_primitive(Box::new(other_variable),
-				variable_declaration)))
+			Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration))
 		},
-		_ => Err(crate::Error::new_not_yet_implemented("todo")),
+		clingo::ast::TermType::BinaryOperation(binary_operation) =>
+		{
+			let operator = crate::translate::common::translate_binary_operator(
+				binary_operation.binary_operator())?;
+
+			match operator
+			{
+				foliage::BinaryOperator::Add
+				| foliage::BinaryOperator::Subtract
+				| foliage::BinaryOperator::Multiply
+					=>
+				{
+					let parameters = (0..2).map(|_| std::rc::Rc::new(
+							foliage::VariableDeclaration::new("<anonymous>".to_string())))
+						.collect::<foliage::VariableDeclarations>();
+
+					let parameter_1 = &parameters[0];
+					let parameter_2 = &parameters[1];
+
+					let translated_binary_operation = foliage::Term::binary_operation(operator,
+						Box::new(foliage::Term::variable(&parameter_1)),
+						Box::new(foliage::Term::variable(&parameter_2)));
+
+					let equals = foliage::Formula::equal(
+						Box::new(foliage::Term::variable(variable_declaration)),
+						Box::new(translated_binary_operation));
+
+					let choose_value_from_left_argument = choose_value_in_term(
+						binary_operation.left(), &parameter_1, &mut function_declarations,
+						&mut variable_declaration_stack)?;
+
+					let choose_value_from_right_argument = choose_value_in_term(
+						binary_operation.right(), &parameter_2, &mut function_declarations,
+						&mut variable_declaration_stack)?;
+
+					let and = foliage::Formula::And(vec![Box::new(equals),
+						Box::new(choose_value_from_left_argument),
+						Box::new(choose_value_from_right_argument)]);
+
+					Ok(foliage::Formula::exists(parameters, Box::new(and)))
+				},
+				foliage::BinaryOperator::Divide
+				| foliage::BinaryOperator::Modulo
+					=>
+				{
+					let parameters = (0..4).map(|_| std::rc::Rc::new(
+							foliage::VariableDeclaration::new("<anonymous>".to_string())))
+						.collect::<foliage::VariableDeclarations>();
+
+					let parameter_i = &parameters[0];
+					let parameter_j = &parameters[1];
+					let parameter_q = &parameters[2];
+					let parameter_r = &parameters[3];
+
+					let j_times_q = foliage::Term::multiply(
+						Box::new(foliage::Term::variable(parameter_j)),
+						Box::new(foliage::Term::variable(parameter_q)));
+
+					let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q),
+						Box::new(foliage::Term::variable(parameter_r)));
+
+					let i_equals_j_times_q_plus_r = foliage::Formula::equal(
+						Box::new(foliage::Term::variable(parameter_j)), Box::new(j_times_q_plus_r));
+
+					let choose_i_in_t1 = choose_value_in_term(binary_operation.left(), parameter_i,
+						&mut function_declarations, &mut variable_declaration_stack)?;
+
+					let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), parameter_j,
+						&mut function_declarations, &mut variable_declaration_stack)?;
+
+					let j_not_equal_to_0 = foliage::Formula::not_equal(
+						Box::new(foliage::Term::variable(parameter_j)),
+						Box::new(foliage::Term::integer(0)));
+
+					let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal(
+						Box::new(foliage::Term::variable(parameter_r)),
+						Box::new(foliage::Term::integer(0)));
+
+					let r_less_than_q = foliage::Formula::less(
+						Box::new(foliage::Term::variable(parameter_r)),
+						Box::new(foliage::Term::variable(parameter_q)));
+
+					let z_equal_to_q = foliage::Formula::equal(
+						Box::new(foliage::Term::variable(variable_declaration)),
+						Box::new(foliage::Term::variable(parameter_q)));
+
+					let z_equal_to_r = foliage::Formula::equal(
+						Box::new(foliage::Term::variable(variable_declaration)),
+						Box::new(foliage::Term::variable(parameter_r)));
+
+					let last_argument = match operator
+					{
+						foliage::BinaryOperator::Divide => z_equal_to_q,
+						foliage::BinaryOperator::Modulo => z_equal_to_r,
+						_ => return Err(crate::Error::new_logic("unreachable code")),
+					};
+
+					let and = foliage::Formula::and(vec![Box::new(i_equals_j_times_q_plus_r),
+						Box::new(choose_i_in_t1), Box::new(choose_i_in_t2),
+						Box::new(j_not_equal_to_0), Box::new(r_greater_or_equal_to_0),
+						Box::new(r_less_than_q), Box::new(last_argument)]);
+
+					Ok(foliage::Formula::exists(parameters, Box::new(and)))
+				},
+				_ => Err(crate::Error::new_not_yet_implemented("todo")),
+			}
+		},
+		clingo::ast::TermType::UnaryOperation(unary_operation) =>
+		{
+			match unary_operation.unary_operator()
+			{
+				clingo::ast::UnaryOperator::Absolute =>
+					return Err(crate::Error::new_unsupported_language_feature("absolute value")),
+				clingo::ast::UnaryOperator::Minus =>
+				{
+					let parameter_z_prime = std::rc::Rc::new(foliage::VariableDeclaration::new(
+						"<anonymous>".to_string()));
+
+					let negative_z_prime = foliage::Term::negative(Box::new(
+						foliage::Term::variable(&parameter_z_prime)));
+					let equals = foliage::Formula::equal(
+						Box::new(foliage::Term::variable(variable_declaration)),
+						Box::new(negative_z_prime));
+
+					let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(),
+						&parameter_z_prime, &mut function_declarations,
+						&mut variable_declaration_stack)?;
+
+					let and = foliage::Formula::and(vec![Box::new(equals),
+						Box::new(choose_z_prime_in_t_prime)]);
+
+					let parameters = vec![parameter_z_prime];
+
+					Ok(foliage::Formula::exists(parameters, Box::new(and)))
+				},
+				_ => Err(crate::Error::new_not_yet_implemented("todo")),
+			}
+		},
+		clingo::ast::TermType::Interval(interval) =>
+		{
+			let parameters = (0..3).map(|_| std::rc::Rc::new(
+					foliage::VariableDeclaration::new("<anonymous>".to_string())))
+				.collect::<foliage::VariableDeclarations>();
+
+			let parameter_i = &parameters[0];
+			let parameter_j = &parameters[1];
+			let parameter_k = &parameters[2];
+
+			let choose_i_in_t_1 = choose_value_in_term(interval.left(), parameter_i,
+				&mut function_declarations, &mut variable_declaration_stack)?;
+
+			let choose_j_in_t_2 = choose_value_in_term(interval.right(), parameter_j,
+				&mut function_declarations, &mut variable_declaration_stack)?;
+
+			let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal(
+				Box::new(foliage::Term::variable(parameter_i)),
+				Box::new(foliage::Term::variable(parameter_k)));
+
+			let k_less_than_or_equal_to_j = foliage::Formula::less_or_equal(
+				Box::new(foliage::Term::variable(parameter_k)),
+				Box::new(foliage::Term::variable(parameter_j)));
+
+			let z_equals_k = foliage::Formula::equal(
+				Box::new(foliage::Term::variable(variable_declaration)),
+				Box::new(foliage::Term::variable(parameter_k)));
+
+			let and = foliage::Formula::and(vec![Box::new(choose_i_in_t_1),
+				Box::new(choose_j_in_t_2), Box::new(i_less_than_or_equal_to_k),
+				Box::new(k_less_than_or_equal_to_j), Box::new(z_equals_k)]);
+
+			Ok(foliage::Formula::exists(parameters, Box::new(and)))
+		},
+		clingo::ast::TermType::Function(_) =>
+			Err(crate::Error::new_unsupported_language_feature("symbolic functions")),
+		clingo::ast::TermType::Pool(_) =>
+			Err(crate::Error::new_unsupported_language_feature("pools")),
+		clingo::ast::TermType::ExternalFunction(_) =>
+			Err(crate::Error::new_unsupported_language_feature("external functions")),
 	}
 }
diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs
index d9d4979..82ab005 100644
--- a/src/translate/verify_properties.rs
+++ b/src/translate/verify_properties.rs
@@ -33,10 +33,7 @@ pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error>
 	let declare_predicate_parameters = |predicate_declaration: &foliage::PredicateDeclaration|
 	{
 		std::rc::Rc::new((0..predicate_declaration.arity)
-			.map(|_| std::rc::Rc::new(foliage::VariableDeclaration
-				{
-					name: "<anonymous>".to_string(),
-				}))
+			.map(|_| std::rc::Rc::new(foliage::VariableDeclaration::new("<anonymous>".to_string())))
 			.collect())
 	};
 
@@ -54,24 +51,47 @@ pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error>
 					});
 			}
 
-			let definitions = definitions.get(&head_atom.predicate_declaration).unwrap();
+			let definitions = definitions.get_mut(&head_atom.predicate_declaration).unwrap();
 
 			variable_declaration_stack.push(std::rc::Rc::clone(&definitions.head_atom_parameters));
 
-			let translated_body = translate_body(rule.body(), &mut function_declarations,
-				&mut predicate_declarations, &mut variable_declaration_stack);
+			let mut definition_arguments = translate_body(rule.body(), &mut function_declarations,
+				&mut predicate_declarations, &mut variable_declaration_stack)?;
+
+			assert_eq!(definitions.head_atom_parameters.len(), head_atom.arguments.len());
+
+			let mut head_atom_arguments_iterator = head_atom.arguments.iter();
+
+			for head_atom_parameter in definitions.head_atom_parameters.iter()
+			{
+				let head_atom_argument = head_atom_arguments_iterator.next().unwrap();
+
+				let translated_head_term = crate::translate::common::choose_value_in_term(
+					head_atom_argument, head_atom_parameter, &mut function_declarations,
+					&mut variable_declaration_stack)?;
+
+				definition_arguments.push(Box::new(translated_head_term));
+			}
 
 			variable_declaration_stack.pop();
+
+			let definition = foliage::Formula::And(definition_arguments);
+
+			let definition = ScopedFormula
+			{
+				free_variable_declarations: variable_declaration_stack.free_variable_declarations,
+				formula: definition,
+			};
+
+			log::trace!("translated formula: {:?}", definition.formula);
+
+			definitions.definitions.push(definition);
 		},
 		HeadType::ChoiceWithSingleAtom(_) =>
 			log::debug!("translating choice rule with single atom"),
 		HeadType::IntegrityConstraint =>
 			log::debug!("translating integrity constraint"),
-		HeadType::Trivial =>
-		{
-			log::debug!("skipping trivial rule");
-			return Ok(());
-		},
+		HeadType::Trivial => log::debug!("skipping trivial rule"),
 	}
 
 	Ok(())
diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs
index b5b5218..4100918 100644
--- a/src/translate/verify_properties/translate_body.rs
+++ b/src/translate/verify_properties/translate_body.rs
@@ -18,29 +18,22 @@ pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::a
 		function.arguments().len());
 
 	let parameters = function.arguments().iter().map(|_| std::rc::Rc::new(
-		foliage::VariableDeclaration
-		{
-			name: "<anonymous>".to_string(),
-		}))
-		.collect::<Vec<_>>();
+		foliage::VariableDeclaration::new("<anonymous>".to_string())))
+		.collect::<foliage::VariableDeclarations>();
 
 	let predicate_arguments = parameters.iter().map(
-		|parameter| Box::new(foliage::Term::Variable(foliage::Variable{declaration: std::rc::Rc::clone(parameter)})))
+		|parameter| Box::new(foliage::Term::variable(parameter)))
 		.collect::<Vec<_>>();
 
-	let predicate = foliage::Predicate
-	{
-		declaration: predicate_declaration,
-		arguments: predicate_arguments,
-	};
+	let predicate = foliage::Formula::predicate(&predicate_declaration, predicate_arguments);
 
 	let predicate_literal = match sign
 	{
 		clingo::ast::Sign::None
 		| clingo::ast::Sign::DoubleNegation
-			=> foliage::Formula::Predicate(predicate),
+			=> predicate,
 		clingo::ast::Sign::Negation
-			=> foliage::Formula::Not(Box::new(foliage::Formula::Predicate(predicate))),
+			=> foliage::Formula::not(Box::new(predicate)),
 	};
 
 	if function.arguments().is_empty()
@@ -48,27 +41,20 @@ pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::a
 		return Ok(predicate_literal);
 	}
 
-	let mut i = 0;
+	assert_eq!(function.arguments().len(), parameters.len());
 
-	let mut arguments = function.arguments().iter().map(|x|
-		{
-			let result = crate::translate::common::choose_value_in_term(x, &parameters[i],
+	let mut parameters_iterator = parameters.iter();
+	let mut arguments = function.arguments().iter().map(
+		|x| crate::translate::common::choose_value_in_term(x, &parameters_iterator.next().unwrap(),
 				&mut function_declarations, &mut variable_declaration_stack)
-				.map(|x| Box::new(x));
-			i += 1;
-			result
-		})
+			.map(|x| Box::new(x)))
 		.collect::<Result<Vec<_>, _>>()?;
 
 	arguments.push(Box::new(predicate_literal));
 
-	let and = foliage::Formula::And(arguments);
+	let and = foliage::Formula::and(arguments);
 
-	Ok(foliage::Formula::Exists(foliage::Exists
-	{
-		parameters,
-		argument: Box::new(and),
-	}))
+	Ok(foliage::Formula::exists(parameters, Box::new(and)))
 }
 
 pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral,
@@ -108,49 +94,32 @@ pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral,
 			&mut variable_declaration_stack),
 		clingo::ast::LiteralType::Comparison(comparison) =>
 		{
-			let new_variable_declaration = || std::rc::Rc::new(foliage::VariableDeclaration
-			{
-				name: "<anonymous>".to_string()
-			});
+			let parameters = (0..2).map(|_| std::rc::Rc::new(foliage::VariableDeclaration::new(
+					"<anonymous>".to_string())))
+				.collect::<foliage::VariableDeclarations>();
 
-			let parameters = vec![new_variable_declaration(), new_variable_declaration()];
+			let mut parameters_iterator = parameters.iter();
+			let parameter_z1 = &parameters_iterator.next().unwrap();
+			let parameter_z2 = &parameters_iterator.next().unwrap();
 
-			let parameter_z1 = &parameters[0];
-			let parameter_z2 = &parameters[1];
+			let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(),
+				parameter_z1, &mut function_declarations, &mut variable_declaration_stack)?;
+			let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(),
+				parameter_z2, &mut function_declarations, &mut variable_declaration_stack)?;
 
-			let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(), &parameter_z1,
-				&mut function_declarations, &mut variable_declaration_stack)?;
-			let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(), &parameter_z2,
-				&mut function_declarations, &mut variable_declaration_stack)?;
+			let variable_1 = foliage::Term::variable(parameter_z1);
+			let variable_2 = foliage::Term::variable(parameter_z2);
 
-			let variable_1 = foliage::Variable
-			{
-				declaration: std::rc::Rc::clone(&parameter_z1),
-			};
+			let operator = crate::translate::common::translate_comparison_operator(
+				comparison.comparison_type());
 
-			let variable_2 = foliage::Variable
-			{
-				declaration: std::rc::Rc::clone(&parameter_z2),
-			};
+			let compare_z1_and_z2 = foliage::Formula::compare(operator, Box::new(variable_1),
+				Box::new(variable_2));
 
-			let comparison_operator
-				= crate::translate::common::translate_comparison_operator(comparison.comparison_type());
+			let and = foliage::Formula::and(vec![Box::new(choose_z1_in_t1),
+				Box::new(choose_z2_in_t2), Box::new(compare_z1_and_z2)]);
 
-			let compare_z1_and_z2 = foliage::Comparison
-			{
-				operator: comparison_operator,
-				left: Box::new(foliage::Term::Variable(variable_1)),
-				right: Box::new(foliage::Term::Variable(variable_2)),
-			};
-
-			let and = foliage::Formula::And(vec![Box::new(choose_z1_in_t1),
-				Box::new(choose_z2_in_t2), Box::new(foliage::Formula::Comparison(compare_z1_and_z2))]);
-
-			Ok(foliage::Formula::Exists(foliage::Exists
-			{
-				parameters,
-				argument: Box::new(and),
-			}))
+			Ok(foliage::Formula::exists(parameters, Box::new(and)))
 		},
 		_ => Err(crate::Error::new_unsupported_language_feature(
 			"body literals other than Booleans, terms, or comparisons")),