diff --git a/src/ast.rs b/src/ast.rs
index 87b91ce..65a3bf3 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -461,7 +461,7 @@ pub enum Formula
 	Predicate(Predicate),
 }
 
-pub type Formulas = Vec<Box<Formula>>;
+pub type Formulas = Vec<Formula>;
 
 impl Formula
 {
diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 6f5085f..194a8e2 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -412,9 +412,9 @@ mod tests
 		format!("{}", formula)
 	}
 
-	fn and(arguments: Formulas) -> Box<Formula>
+	fn and(arguments: Vec<Box<Formula>>) -> Box<Formula>
 	{
-		Box::new(Formula::and(arguments))
+		Box::new(Formula::and(arguments.into_iter().map(|x| *x).collect()))
 	}
 
 	fn equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
@@ -447,9 +447,9 @@ mod tests
 		Box::new(Formula::greater_or_equal(left, right))
 	}
 
-	fn if_and_only_if(arguments: Formulas) -> Box<Formula>
+	fn if_and_only_if(arguments: Vec<Box<Formula>>) -> Box<Formula>
 	{
-		Box::new(Formula::if_and_only_if(arguments))
+		Box::new(Formula::if_and_only_if(arguments.into_iter().map(|x| *x).collect()))
 	}
 
 	fn implies(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
@@ -478,9 +478,9 @@ mod tests
 		Box::new(Formula::not_equal(left, right))
 	}
 
-	fn or(arguments: Formulas) -> Box<Formula>
+	fn or(arguments: Vec<Box<Formula>>) -> Box<Formula>
 	{
-		Box::new(Formula::or(arguments))
+		Box::new(Formula::or(arguments.into_iter().map(|x| *x).collect()))
 	}
 
 	fn predicate(name: &str, arguments: Terms) -> Box<Formula>
@@ -578,22 +578,22 @@ mod tests
 		predicate("r", vec![])
 	}
 
-	fn pqr() -> Formulas
+	fn pqr() -> Vec<Box<Formula>>
 	{
 		vec![p(), q(), r()]
 	}
 
-	fn p1q1r1() -> Formulas
+	fn p1q1r1() -> Vec<Box<Formula>>
 	{
 		vec![p1(), q1(), predicate("r1", vec![])]
 	}
 
-	fn p2q2r2() -> Formulas
+	fn p2q2r2() -> Vec<Box<Formula>>
 	{
 		vec![p2(), q2(), predicate("r2", vec![])]
 	}
 
-	fn p3q3r3() -> Formulas
+	fn p3q3r3() -> Vec<Box<Formula>>
 	{
 		vec![p3(), q3(), predicate("r3", vec![])]
 	}
diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs
index a7da5cd..0d71675 100644
--- a/src/parse/formulas.rs
+++ b/src/parse/formulas.rs
@@ -67,7 +67,7 @@ fn not<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
 	)(i)
 }
 
-fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
+fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 {
 	map_res
 	(
@@ -89,7 +89,7 @@ fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Form
 		{
 			if arguments.len() >= 2
 			{
-				Ok(arguments.into_iter().map(Box::new).collect())
+				Ok(arguments.into_iter().collect())
 			}
 			else
 			{
@@ -99,7 +99,7 @@ fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Form
 	)(i)
 }
 
-fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
+fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 {
 	map_res
 	(
@@ -121,7 +121,7 @@ fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formu
 		{
 			if arguments.len() >= 2
 			{
-				Ok(arguments.into_iter().map(Box::new).collect())
+				Ok(arguments.into_iter().collect())
 			}
 			else
 			{
@@ -187,7 +187,7 @@ fn implies_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, c
 	)(i)
 }
 
-fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
+fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 {
 	map_res
 	(
@@ -205,7 +205,7 @@ fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<
 		{
 			if arguments.len() >= 2
 			{
-				Ok(arguments.into_iter().map(Box::new).collect())
+				Ok(arguments.into_iter().collect())
 			}
 			else
 			{
@@ -535,15 +535,15 @@ mod tests
 
 		assert_eq!(format_formula("(true  and  false)"), "true and false");
 		assert_eq!(formula_as_and("(true and false)").len(), 2);
-		assert_eq!(*formula_as_and("(true and false)").remove(0), Formula::true_());
-		assert_eq!(*formula_as_and("(true and false)").remove(1), Formula::false_());
+		assert_eq!(formula_as_and("(true and false)").remove(0), Formula::true_());
+		assert_eq!(formula_as_and("(true and false)").remove(1), Formula::false_());
 		// The order of elements is retained
 		assert_ne!(formula("(true and false)"), formula("false and true"));
 		assert_eq!(format_formula("(p  and  q  and  r  and  s)"), "p and q and r and s");
 		assert_eq!(
-			as_predicate(*formula_as_and("(p and q and r and s)").remove(0)).declaration.name, "p");
+			as_predicate(formula_as_and("(p and q and r and s)").remove(0)).declaration.name, "p");
 		assert_eq!(
-			as_predicate(*formula_as_and("(p and q and r and s)").remove(3)).declaration.name, "s");
+			as_predicate(formula_as_and("(p and q and r and s)").remove(3)).declaration.name, "s");
 
 		let formula = |i| original::formula(i, &Declarations::new());
 
@@ -575,15 +575,15 @@ mod tests
 
 		assert_eq!(format_formula("(true  or  false)"), "true or false");
 		assert_eq!(formula_as_or("(true or false)").len(), 2);
-		assert_eq!(*formula_as_or("(true or false)").remove(0), Formula::true_());
-		assert_eq!(*formula_as_or("(true or false)").remove(1), Formula::false_());
+		assert_eq!(formula_as_or("(true or false)").remove(0), Formula::true_());
+		assert_eq!(formula_as_or("(true or false)").remove(1), Formula::false_());
 		// The order of elements is retained
 		assert_ne!(formula("(true or false)"), formula("false or true)"));
 		assert_eq!(format_formula("(p  or  q  or  r  or  s)"), "p or q or r or s");
 		assert_eq!(
-			as_predicate(*formula_as_or("(p or q or r or s)").remove(0)).declaration.name, "p");
+			as_predicate(formula_as_or("(p or q or r or s)").remove(0)).declaration.name, "p");
 		assert_eq!(
-			as_predicate(*formula_as_or("(p or q or r or s)").remove(3)).declaration.name, "s");
+			as_predicate(formula_as_or("(p or q or r or s)").remove(3)).declaration.name, "s");
 
 		let formula = |i| original::formula(i, &Declarations::new());