diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 00163ad..47d25f0 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -967,301 +967,57 @@ mod tests
 	fn format_combination_quantified_formula_and_lower()
 	{
 		// Quantified formula + quantified formula
-		assert_eq!(format(
-			exists(x1y1z1(), exists(x2y2z2(), p()))),
+		assert_all!(i, exists(x1y1z1(), i(exists(x2y2z2(), p()))),
 			"exists X1, Y1, Z1 exists X2, Y2, Z2 p");
-		assert_eq!(format(
-			exists(x1y1z1(), and(vec![exists(x2y2z2(), p())]))),
-			"exists X1, Y1, Z1 exists X2, Y2, Z2 p");
-		assert_eq!(format(
-			exists(x1y1z1(), or(vec![exists(x2y2z2(), p())]))),
-			"exists X1, Y1, Z1 exists X2, Y2, Z2 p");
-		assert_eq!(format(
-			exists(x1y1z1(), if_and_only_if(vec![exists(x2y2z2(), p())]))),
-			"exists X1, Y1, Z1 exists X2, Y2, Z2 p");
-		assert_eq!(format(
-			exists(x1y1z1(), for_all(x2y2z2(), p()))),
+		assert_all!(i, exists(x1y1z1(), i(for_all(x2y2z2(), p()))),
 			"exists X1, Y1, Z1 forall X2, Y2, Z2 p");
-		assert_eq!(format(
-			exists(x1y1z1(), and(vec![for_all(x2y2z2(), p())]))),
-			"exists X1, Y1, Z1 forall X2, Y2, Z2 p");
-		assert_eq!(format(
-			exists(x1y1z1(), or(vec![for_all(x2y2z2(), p())]))),
-			"exists X1, Y1, Z1 forall X2, Y2, Z2 p");
-		assert_eq!(format(
-			exists(x1y1z1(), if_and_only_if(vec![for_all(x2y2z2(), p())]))),
-			"exists X1, Y1, Z1 forall X2, Y2, Z2 p");
-		assert_eq!(format(
-			for_all(x1y1z1(), exists(x2y2z2(), p()))),
+		assert_all!(i, for_all(x1y1z1(), i(exists(x2y2z2(), p()))),
 			"forall X1, Y1, Z1 exists X2, Y2, Z2 p");
-		assert_eq!(format(
-			for_all(x1y1z1(), and(vec![exists(x2y2z2(), p())]))),
-			"forall X1, Y1, Z1 exists X2, Y2, Z2 p");
-		assert_eq!(format(
-			for_all(x1y1z1(), or(vec![exists(x2y2z2(), p())]))),
-			"forall X1, Y1, Z1 exists X2, Y2, Z2 p");
-		assert_eq!(format(
-			for_all(x1y1z1(), if_and_only_if(vec![exists(x2y2z2(), p())]))),
-			"forall X1, Y1, Z1 exists X2, Y2, Z2 p");
-		assert_eq!(format(
-			for_all(x1y1z1(), for_all(x2y2z2(), p()))),
-			"forall X1, Y1, Z1 forall X2, Y2, Z2 p");
-		assert_eq!(format(
-			for_all(x1y1z1(),
-				and(vec![for_all(x2y2z2(), p())]))),
-			"forall X1, Y1, Z1 forall X2, Y2, Z2 p");
-		assert_eq!(format(
-			for_all(x1y1z1(),
-				or(vec![for_all(x2y2z2(), p())]))),
-			"forall X1, Y1, Z1 forall X2, Y2, Z2 p");
-		assert_eq!(format(
-			for_all(x1y1z1(), if_and_only_if(vec![for_all(x2y2z2(), p())]))),
+		assert_all!(i, for_all(x1y1z1(), i(for_all(x2y2z2(), p()))),
 			"forall X1, Y1, Z1 forall X2, Y2, Z2 p");
 
 		// Quantified formula + and
-		assert_eq!(format(exists(xyz(), and(pqr()))), "exists X, Y, Z (p and q and r)");
-		assert_eq!(format(exists(xyz(), and(pqr()))), "exists X, Y, Z (p and q and r)");
-		assert_eq!(format(exists(xyz(), or(vec![and(pqr())]))), "exists X, Y, Z (p and q and r)");
-		assert_eq!(format(
-			exists(xyz(), if_and_only_if(vec![and(pqr())]))),
-			"exists X, Y, Z (p and q and r)");
-		assert_eq!(format(
-			and(vec![exists(x1y1z1(), p()), exists(x2y2z2(), q()), exists(x3y3z3(), r())])),
+		assert_all!(i, exists(xyz(), i(and(pqr()))), "exists X, Y, Z (p and q and r)");
+		assert_all!(i, and(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())),
+			i(exists(x3y3z3(), r()))]),
 			"exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			and(vec![and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]),
-				and(vec![exists(x3y3z3(), r())])])),
-			"exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			and(vec![or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]),
-				or(vec![exists(x3y3z3(), r())])])),
-			"exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![exists(x1y1z1(), p())]),
-				if_and_only_if(vec![exists(x2y2z2(), q())]),
-				if_and_only_if(vec![exists(x3y3z3(), r())])])),
-			"exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r");
-		assert_eq!(format(for_all(xyz(), and(pqr()))), "forall X, Y, Z (p and q and r)");
-		assert_eq!(format(for_all(xyz(), and(vec![and(pqr())]))), "forall X, Y, Z (p and q and r)");
-		assert_eq!(format(for_all(xyz(), or(vec![and(pqr())]))), "forall X, Y, Z (p and q and r)");
-		assert_eq!(format(
-			for_all(xyz(), if_and_only_if(vec![and(pqr())]))),
-			"forall X, Y, Z (p and q and r)");
-		assert_eq!(format(
-			and(vec![for_all(x1y1z1(), p()), for_all(x2y2z2(), q()), for_all(x3y3z3(), r())])),
-			"forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r");
-		assert_eq!(format(
-			and(vec![and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]),
-				and(vec![for_all(x3y3z3(), r())])])),
-			"forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r");
-		assert_eq!(format(
-			and(vec![or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]),
-				or(vec![for_all(x3y3z3(), r())])])),
-			"forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![for_all(x1y1z1(), p())]),
-				if_and_only_if(vec![for_all(x2y2z2(), q())]),
-				if_and_only_if(vec![for_all(x3y3z3(), r())])])),
+		assert_all!(i, for_all(xyz(), i(and(pqr()))), "forall X, Y, Z (p and q and r)");
+		assert_all!(i, and(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())),
+			i(for_all(x3y3z3(), r()))]),
 			"forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r");
 
 		// Quantified formula + or
-		assert_eq!(format(exists(xyz(), or(pqr()))), "exists X, Y, Z (p or q or r)");
-		assert_eq!(format(exists(xyz(), and(vec![or(pqr())]))), "exists X, Y, Z (p or q or r)");
-		assert_eq!(format(exists(xyz(), or(vec![or(pqr())]))), "exists X, Y, Z (p or q or r)");
-		assert_eq!(format(
-			exists(xyz(), if_and_only_if(vec![or(pqr())]))),
-			"exists X, Y, Z (p or q or r)");
-		assert_eq!(format(
-			or(vec![exists(x1y1z1(), p()), exists(x2y2z2(), q()), exists(x3y3z3(), r())])),
+		assert_all!(i, exists(xyz(), i(or(pqr()))), "exists X, Y, Z (p or q or r)");
+		assert_all!(i, or(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())),
+			i(exists(x3y3z3(), r()))]),
 			"exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			or(vec![and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]),
-				and(vec![exists(x3y3z3(), r())])])),
-			"exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			or(vec![or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]),
-				or(vec![exists(x3y3z3(), r())])])),
-			"exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![exists(x1y1z1(), p())]),
-				if_and_only_if(vec![exists(x2y2z2(), q())]),
-				if_and_only_if(vec![exists(x3y3z3(), r())])])),
-			"exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r");
-		assert_eq!(format(for_all(xyz(), or(pqr()))), "forall X, Y, Z (p or q or r)");
-		assert_eq!(format(for_all(xyz(), and(vec![or(pqr())]))), "forall X, Y, Z (p or q or r)");
-		assert_eq!(format(for_all(xyz(), or(vec![or(pqr())]))), "forall X, Y, Z (p or q or r)");
-		assert_eq!(format(for_all(xyz(),
-			if_and_only_if(vec![or(pqr())]))),
-			"forall X, Y, Z (p or q or r)");
-		assert_eq!(format(
-			or(vec![for_all(x1y1z1(), p()), for_all(x2y2z2(), q()), for_all(x3y3z3(), r())])),
-			"forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r");
-		assert_eq!(format(
-			or(vec![and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]),
-				and(vec![for_all(x3y3z3(), r())])])),
-			"forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r");
-		assert_eq!(format(
-			or(vec![or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]),
-				or(vec![for_all(x3y3z3(), r())])])),
-			"forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![for_all(x1y1z1(), p())]),
-				if_and_only_if(vec![for_all(x2y2z2(), q())]),
-				if_and_only_if(vec![for_all(x3y3z3(), r())])])),
+		assert_all!(i, for_all(xyz(), i(or(pqr()))), "forall X, Y, Z (p or q or r)");
+		assert_all!(i, or(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())),
+			i(for_all(x3y3z3(), r()))]),
 			"forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r");
 
 		// Quantified formula + implies
-		assert_eq!(format(exists(xyz(), implies_right(p(), q()))), "exists X, Y, Z (p -> q)");
-		assert_eq!(format(
-			exists(xyz(), and(vec![implies_right(p(), q())]))),
-			"exists X, Y, Z (p -> q)");
-		assert_eq!(format(
-			exists(xyz(), or(vec![implies_right(p(), q())]))),
-			"exists X, Y, Z (p -> q)");
-		assert_eq!(format(
-			exists(xyz(), if_and_only_if(vec![implies_right(p(), q())]))),
-			"exists X, Y, Z (p -> q)");
-		assert_eq!(format(exists(xyz(), implies_left(p(), q()))), "exists X, Y, Z (q <- p)");
-		assert_eq!(format(
-			exists(xyz(), and(vec![implies_left(p(), q())]))),
-			"exists X, Y, Z (q <- p)");
-		assert_eq!(format(
-			exists(xyz(), or(vec![implies_left(p(), q())]))),
-			"exists X, Y, Z (q <- p)");
-		assert_eq!(format(
-			exists(xyz(), if_and_only_if(vec![implies_left(p(), q())]))),
-			"exists X, Y, Z (q <- p)");
-		assert_eq!(format(
-			implies_right(exists(x1y1z1(), p()), exists(x2y2z2(), q()))),
+		assert_all!(i, exists(xyz(), i(implies_right(p(), q()))), "exists X, Y, Z (p -> q)");
+		assert_all!(i, exists(xyz(), i(implies_left(p(), q()))), "exists X, Y, Z (q <- p)");
+		assert_all!(i, implies_right(i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q()))),
 			"exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q");
-		assert_eq!(format(
-			implies_right(and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]))),
-			"exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q");
-		assert_eq!(format(
-			implies_right(or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]))),
-			"exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q");
-		assert_eq!(format(
-			implies_right(if_and_only_if(vec![exists(x1y1z1(), p())]),
-				if_and_only_if(vec![exists(x2y2z2(), q())]))),
-			"exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q");
-		assert_eq!(format(
-			implies_left(exists(x1y1z1(), p()), exists(x2y2z2(), q()))),
+		assert_all!(i, implies_left(i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q()))),
 			"exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p");
-		assert_eq!(format(
-			implies_left(and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]))),
-			"exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p");
-		assert_eq!(format(
-			implies_left(or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]))),
-			"exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p");
-		assert_eq!(format(
-			implies_left(if_and_only_if(vec![exists(x1y1z1(), p())]),
-				if_and_only_if(vec![exists(x2y2z2(), q())]))),
-			"exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p");
-		assert_eq!(format(for_all(xyz(), implies_right(p(), q()))), "forall X, Y, Z (p -> q)");
-		assert_eq!(format(
-			for_all(xyz(), and(vec![implies_right(p(), q())]))),
-			"forall X, Y, Z (p -> q)");
-		assert_eq!(format(
-			for_all(xyz(), or(vec![implies_right(p(), q())]))),
-			"forall X, Y, Z (p -> q)");
-		assert_eq!(format(
-			for_all(xyz(), if_and_only_if(vec![implies_right(p(), q())]))),
-			"forall X, Y, Z (p -> q)");
-		assert_eq!(format(
-			for_all(xyz(), implies_left(p(), q()))),
-			"forall X, Y, Z (q <- p)");
-		assert_eq!(format(
-			for_all(xyz(), and(vec![implies_left(p(), q())]))),
-			"forall X, Y, Z (q <- p)");
-		assert_eq!(format(
-			for_all(xyz(), or(vec![implies_left(p(), q())]))),
-			"forall X, Y, Z (q <- p)");
-		assert_eq!(format(
-			for_all(xyz(), if_and_only_if(vec![implies_left(p(), q())]))),
-			"forall X, Y, Z (q <- p)");
-		assert_eq!(format(
-			implies_right(for_all(x1y1z1(), p()), for_all(x2y2z2(), q()))),
+		assert_all!(i, for_all(xyz(), i(implies_right(p(), q()))), "forall X, Y, Z (p -> q)");
+		assert_all!(i, for_all(xyz(), i(implies_left(p(), q()))), "forall X, Y, Z (q <- p)");
+		assert_all!(i, implies_right(i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q()))),
 			"forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q");
-		assert_eq!(format(
-			implies_right(and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]))),
-			"forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q");
-		assert_eq!(format(
-			implies_right(or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]))),
-			"forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q");
-		assert_eq!(format(
-			implies_right(if_and_only_if(vec![for_all(x1y1z1(), p())]),
-				if_and_only_if(vec![for_all(x2y2z2(), q())]))),
-			"forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q");
-		assert_eq!(format(
-			implies_left(for_all(x1y1z1(), p()), for_all(x2y2z2(), q()))),
-			"forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p");
-		assert_eq!(format(
-			implies_left(and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]))),
-			"forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p");
-		assert_eq!(format(
-			implies_left(or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]))),
-			"forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p");
-		assert_eq!(format(
-			implies_left(if_and_only_if(vec![for_all(x1y1z1(), p())]),
-				if_and_only_if(vec![for_all(x2y2z2(), q())]))),
+		assert_all!(i, implies_left(i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q()))),
 			"forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p");
 
 		// Quantified formula + if and only if
-		assert_eq!(format(exists(xyz(), if_and_only_if(pqr()))), "exists X, Y, Z (p <-> q <-> r)");
-		assert_eq!(format(
-			exists(xyz(), and(vec![if_and_only_if(pqr())]))),
-			"exists X, Y, Z (p <-> q <-> r)");
-		assert_eq!(format(
-			exists(xyz(), or(vec![if_and_only_if(pqr())]))),
-			"exists X, Y, Z (p <-> q <-> r)");
-		assert_eq!(format(
-			exists(xyz(), if_and_only_if(vec![if_and_only_if(pqr())]))),
-			"exists X, Y, Z (p <-> q <-> r)");
-		assert_eq!(format(
-			if_and_only_if(vec![exists(x1y1z1(), p()), exists(x2y2z2(), q()),
-				exists(x3y3z3(), r())])),
+		assert_all!(i, exists(xyz(), i(if_and_only_if(pqr()))), "exists X, Y, Z (p <-> q <-> r)");
+		assert_all!(i, if_and_only_if(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())),
+			i(exists(x3y3z3(), r()))]),
 			"exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]),
-				and(vec![exists(x3y3z3(), r())])])),
-			"exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]),
-				or(vec![exists(x3y3z3(), r())])])),
-			"exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			if_and_only_if(vec![if_and_only_if(vec![exists(x1y1z1(), p())]),
-				if_and_only_if(vec![exists(x2y2z2(), q())]),
-				if_and_only_if(vec![exists(x3y3z3(), r())])])),
-			"exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r");
-		assert_eq!(format(
-			for_all(xyz(), if_and_only_if(pqr()))),
-			"forall X, Y, Z (p <-> q <-> r)");
-		assert_eq!(format(
-			for_all(xyz(), and(vec![if_and_only_if(pqr())]))),
-			"forall X, Y, Z (p <-> q <-> r)");
-		assert_eq!(format(
-			for_all(xyz(), or(vec![if_and_only_if(pqr())]))),
-			"forall X, Y, Z (p <-> q <-> r)");
-		assert_eq!(format(
-			for_all(xyz(), if_and_only_if(vec![if_and_only_if(pqr())]))),
-			"forall X, Y, Z (p <-> q <-> r)");
-		assert_eq!(format(
-			if_and_only_if(vec![for_all(x1y1z1(), p()), for_all(x2y2z2(), q()),
-				for_all(x3y3z3(), r())])),
-			"forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r");
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![for_all(x1y1z1(), p())]),
-				and(vec![for_all(x2y2z2(), q())]), and(vec![for_all(x3y3z3(), r())])])),
-			"forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r");
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]),
-				or(vec![for_all(x3y3z3(), r())])])),
-			"forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r");
-		assert_eq!(format(
-			if_and_only_if(vec![if_and_only_if(vec![for_all(x1y1z1(), p())]),
-				if_and_only_if(vec![for_all(x2y2z2(), q())]),
-				if_and_only_if(vec![for_all(x3y3z3(), r())])])),
+		assert_all!(i, for_all(xyz(), i(if_and_only_if(pqr()))), "forall X, Y, Z (p <-> q <-> r)");
+		assert_all!(i, if_and_only_if(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())),
+			i(for_all(x3y3z3(), r()))]),
 			"forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r");
 	}
 
@@ -1269,204 +1025,46 @@ mod tests
 	fn format_combination_and_and_lower()
 	{
 		// And + and
-		assert_eq!(format(
-			and(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])),
+		assert_all!(i, and(vec![i(and(vec![p()])), i(and(vec![q()])), i(and(vec![r()]))]),
 			"p and q and r");
-		assert_eq!(format(
-			and(vec![and(vec![and(vec![p()])]), and(vec![and(vec![q()])]),
-				and(vec![and(vec![r()])])])),
-			"p and q and r");
-		assert_eq!(format(
-			and(vec![or(vec![and(vec![p()])]), or(vec![and(vec![q()])]),
-				or(vec![and(vec![r()])])])),
-			"p and q and r");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![and(vec![p()])]), if_and_only_if(vec![and(vec![q()])]),
-				if_and_only_if(vec![and(vec![r()])])])),
-			"p and q and r");
-		assert_eq!(format(
-			and(vec![and(p1q1r1()), and(p2q2r2()), and(p3q3r3())])),
-			"p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3");
-		assert_eq!(format(
-			and(vec![and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]),
-				and(vec![and(p3q3r3())])])),
-			"p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3");
-		assert_eq!(format(
-			and(vec![or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]), or(vec![and(p3q3r3())])])),
-			"p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![and(p1q1r1())]), if_and_only_if(vec![and(p2q2r2())]),
-				if_and_only_if(vec![and(p3q3r3())])])),
+		assert_all!(i, and(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]),
 			"p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3");
 
 		// And + or
-		assert_eq!(format(and(vec![or(vec![p()]), or(vec![q()]), or(vec![r()])])), "p and q and r");
-		assert_eq!(format(
-			and(vec![and(vec![or(vec![p()])]), and(vec![or(vec![q()])]),
-				and(vec![or(vec![r()])])])),
-			"p and q and r");
-		assert_eq!(format(
-			and(vec![or(vec![or(vec![p()])]), or(vec![or(vec![q()])]), or(vec![or(vec![r()])])])),
-			"p and q and r");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![or(vec![p()])]), if_and_only_if(vec![or(vec![q()])]),
-				if_and_only_if(vec![or(vec![r()])])])),
+		assert_all!(i, and(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]),
 			"p and q and r");
 		assert_all!(i, and(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]),
 			"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
 
-		assert_eq!(format(or(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])), "p or q or r");
-		assert_eq!(format(
-			or(vec![and(vec![and(vec![p()])]), and(vec![and(vec![q()])]),
-				and(vec![and(vec![r()])])])),
+		assert_all!(i, or(vec![i(and(vec![p()])), i(and(vec![q()])), i(and(vec![r()]))]),
 			"p or q or r");
-		assert_eq!(format(
-			or(vec![or(vec![and(vec![p()])]), or(vec![and(vec![q()])]), or(vec![and(vec![r()])])])),
-			"p or q or r");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![and(vec![p()])]), if_and_only_if(vec![and(vec![q()])]),
-				if_and_only_if(vec![and(vec![r()])])])),
-			"p or q or r");
-		assert_eq!(format(
-			or(vec![and(p1q1r1()), and(p2q2r2()), and(p3q3r3())])),
-			"p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3");
-		assert_eq!(format(
-			or(vec![and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]), and(vec![and(p3q3r3())])])),
-			"p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3");
-		assert_eq!(format(
-			or(vec![or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]), or(vec![and(p3q3r3())])])),
-			"p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![and(p1q1r1())]), if_and_only_if(vec![and(p2q2r2())]),
-				if_and_only_if(vec![and(p3q3r3())])])),
+		assert_all!(i, or(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]),
 			"p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3");
 
 		// And + implies
-		assert_eq!(format(
-			and(vec![implies_right(p1(), q1()), implies_right(p2(), q2()),
-				implies_right(p3(), q3())])),
+		assert_all!(i, and(vec![i(implies_right(p1(), q1())), i(implies_right(p2(), q2())),
+			i(implies_right(p3(), q3()))]),
 			"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
-		assert_eq!(format(
-			and(vec![and(vec![implies_right(p1(), q1())]), and(vec![implies_right(p2(), q2())]),
-				and(vec![implies_right(p3(), q3())])])),
-			"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
-		assert_eq!(format(
-			and(vec![or(vec![implies_right(p1(), q1())]), or(vec![implies_right(p2(), q2())]),
-				or(vec![implies_right(p3(), q3())])])),
-			"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![implies_right(p1(), q1())]),
-				if_and_only_if(vec![implies_right(p2(), q2())]),
-				if_and_only_if(vec![implies_right(p3(), q3())])])),
-			"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
-		assert_eq!(format(
-			and(vec![implies_left(p1(), q1()), implies_left(p2(), q2()),
-				implies_left(p3(), q3())])),
+		assert_all!(i, and(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())),
+			i(implies_left(p3(), q3()))]),
 			"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
-		assert_eq!(format(
-			and(vec![and(vec![implies_left(p1(), q1())]), and(vec![implies_left(p2(), q2())]),
-				and(vec![implies_left(p3(), q3())])])),
-			"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
-		assert_eq!(format(
-			and(vec![or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]),
-				or(vec![implies_left(p3(), q3())])])),
-			"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![implies_left(p1(), q1())]),
-				if_and_only_if(vec![implies_left(p2(), q2())]),
-				if_and_only_if(vec![implies_left(p3(), q3())])])),
-			"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
-		assert_eq!(format(
-			implies_right(and(p1q1r1()), and(p2q2r2()))),
+		assert_all!(i, implies_right(i(and(p1q1r1())), i(and(p2q2r2()))),
 			"p1 and q1 and r1 -> p2 and q2 and r2");
-		assert_eq!(format(
-			implies_right(and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]))),
-			"p1 and q1 and r1 -> p2 and q2 and r2");
-		assert_eq!(format(
-			implies_right(or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]))),
-			"p1 and q1 and r1 -> p2 and q2 and r2");
-		assert_eq!(format(
-			implies_right(if_and_only_if(vec![and(p1q1r1())]),
-				if_and_only_if(vec![and(p2q2r2())]))),
-			"p1 and q1 and r1 -> p2 and q2 and r2");
-		assert_eq!(format(
-			implies_left(and(p1q1r1()), and(p2q2r2()))),
-			"p2 and q2 and r2 <- p1 and q1 and r1");
-		assert_eq!(format(
-			implies_left(and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]))),
-			"p2 and q2 and r2 <- p1 and q1 and r1");
-		assert_eq!(format(
-			implies_left(or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]))),
-			"p2 and q2 and r2 <- p1 and q1 and r1");
-		assert_eq!(format(
-			implies_left(if_and_only_if(vec![and(p1q1r1())]), if_and_only_if(vec![and(p2q2r2())]))),
+		assert_all!(i, implies_left(i(and(p1q1r1())), i(and(p2q2r2()))),
 			"p2 and q2 and r2 <- p1 and q1 and r1");
 
 		// And + if and only if
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![p()]), if_and_only_if(vec![q()]),
-				if_and_only_if(vec![r()])])),
+		assert_all!(i, and(vec![i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()])),
+			i(if_and_only_if(vec![r()]))]),
 			"p and q and r");
-		assert_eq!(format(
-			and(vec![and(vec![if_and_only_if(vec![p()])]), and(vec![if_and_only_if(vec![q()])]),
-				and(vec![if_and_only_if(vec![r()])])])),
-			"p and q and r");
-		assert_eq!(format(
-			and(vec![or(vec![if_and_only_if(vec![p()])]), or(vec![if_and_only_if(vec![q()])]),
-				or(vec![if_and_only_if(vec![r()])])])),
-			"p and q and r");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![if_and_only_if(vec![p()])]),
-				if_and_only_if(vec![if_and_only_if(vec![q()])]),
-				if_and_only_if(vec![if_and_only_if(vec![r()])])])),
-			"p and q and r");
-		assert_eq!(format(
-			and(vec![if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()),
-				if_and_only_if(p3q3r3())])),
-			"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
-		assert_eq!(format(
-			and(vec![and(vec![if_and_only_if(p1q1r1())]), and(vec![if_and_only_if(p2q2r2())]),
-				and(vec![if_and_only_if(p3q3r3())])])),
-			"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
-		assert_eq!(format(
-			and(vec![or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]),
-				or(vec![if_and_only_if(p3q3r3())])])),
-			"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
-		assert_eq!(format(
-			and(vec![if_and_only_if(vec![if_and_only_if(p1q1r1())]),
-				if_and_only_if(vec![if_and_only_if(p2q2r2())]),
-				if_and_only_if(vec![if_and_only_if(p3q3r3())])])),
+		assert_all!(i, and(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())),
+			i(if_and_only_if(p3q3r3()))]),
 			"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
 
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])),
+		assert_all!(i, if_and_only_if(vec![i(and(vec![p()])), i(and(vec![q()])),
+			i(and(vec![r()]))]),
 			"p <-> q <-> r");
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![and(vec![p()])]), and(vec![and(vec![q()])]),
-				and(vec![and(vec![r()])])])),
-			"p <-> q <-> r");
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![and(vec![p()])]), or(vec![and(vec![q()])]),
-				or(vec![and(vec![r()])])])),
-			"p <-> q <-> r");
-		assert_eq!(format(
-			if_and_only_if(vec![if_and_only_if(vec![and(vec![p()])]),
-				if_and_only_if(vec![and(vec![q()])]), if_and_only_if(vec![and(vec![r()])])])),
-			"p <-> q <-> r");
-		assert_eq!(format(
-			if_and_only_if(vec![and(p1q1r1()), and(p2q2r2()), and(p3q3r3())])),
-			"p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3");
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]),
-				and(vec![and(p3q3r3())])])),
-			"p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3");
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]),
-				or(vec![and(p3q3r3())])])),
-			"p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3");
-		assert_eq!(format(
-			if_and_only_if(vec![if_and_only_if(vec![and(p1q1r1())]),
-				if_and_only_if(vec![and(p2q2r2())]), if_and_only_if(vec![and(p3q3r3())])])),
+		assert_all!(i, if_and_only_if(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]),
 			"p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3");
 	}
 
@@ -1474,160 +1072,37 @@ mod tests
 	fn format_combination_or_and_lower()
 	{
 		// Or + or
-		assert_eq!(format(
-			or(vec![or(vec![p()]), or(vec![q()]), or(vec![r()])])),
+		assert_all!(i, or(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]),
 			"p or q or r");
-		assert_eq!(format(
-			or(vec![and(vec![or(vec![p()])]), and(vec![or(vec![q()])]), and(vec![or(vec![r()])])])),
-			"p or q or r");
-		assert_eq!(format(
-			or(vec![or(vec![or(vec![p()])]), or(vec![or(vec![q()])]),
-				or(vec![or(vec![r()])])])),
-			"p or q or r");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![or(vec![p()])]), if_and_only_if(vec![or(vec![q()])]),
-				if_and_only_if(vec![or(vec![r()])])])),
-			"p or q or r");
-		assert_eq!(format(
-			or(vec![or(p1q1r1()), or(p2q2r2()), or(p3q3r3())])),
-			"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
-		assert_eq!(format(
-			or(vec![and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]), and(vec![or(p3q3r3())])])),
-			"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
-		assert_eq!(format(
-			or(vec![or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]), or(vec![or(p3q3r3())])])),
-			"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![or(p1q1r1())]), if_and_only_if(vec![or(p2q2r2())]),
-				if_and_only_if(vec![or(p3q3r3())])])),
+		assert_all!(i, or(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]),
 			"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
 
 		// Or + implies
-		assert_eq!(format(
-			or(vec![implies_right(p1(), q1()), implies_right(p2(), q2()),
-				implies_right(p3(), q3())])),
+		assert_all!(i, or(vec![i(implies_right(p1(), q1())), i(implies_right(p2(), q2())),
+			i(implies_right(p3(), q3()))]),
 			"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
-		assert_eq!(format(
-			or(vec![and(vec![implies_right(p1(), q1())]), and(vec![implies_right(p2(), q2())]),
-				and(vec![implies_right(p3(), q3())])])),
+		assert_all!(i, or(vec![i(and(vec![implies_right(p1(), q1())])),
+			i(and(vec![implies_right(p2(), q2())])), i(and(vec![implies_right(p3(), q3())]))]),
 			"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
-		assert_eq!(format(
-			or(vec![or(vec![implies_right(p1(), q1())]), or(vec![implies_right(p2(), q2())]),
-				or(vec![implies_right(p3(), q3())])])),
-			"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![implies_right(p1(), q1())]),
-				if_and_only_if(vec![implies_right(p2(), q2())]),
-				if_and_only_if(vec![implies_right(p3(), q3())])])),
-			"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
-		assert_eq!(format(
-			or(vec![implies_left(p1(), q1()), implies_left(p2(), q2()),
-				implies_left(p3(), q3())])),
+		assert_all!(i, or(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())),
+			i(implies_left(p3(), q3()))]),
 			"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
-		assert_eq!(format(
-			or(vec![and(vec![implies_left(p1(), q1())]), and(vec![implies_left(p2(), q2())]),
-				and(vec![implies_left(p3(), q3())])])),
-			"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
-		assert_eq!(format(
-			or(vec![or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]),
-				or(vec![implies_left(p3(), q3())])])),
-			"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![implies_left(p1(), q1())]),
-				if_and_only_if(vec![implies_left(p2(), q2())]),
-				if_and_only_if(vec![implies_left(p3(), q3())])])),
-			"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
-		assert_eq!(format(
-			implies_right(or(p1q1r1()), or(p2q2r2()))),
+		assert_all!(i, implies_right(i(or(p1q1r1())), i(or(p2q2r2()))),
 			"p1 or q1 or r1 -> p2 or q2 or r2");
-		assert_eq!(format(
-			implies_right(and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]))),
-			"p1 or q1 or r1 -> p2 or q2 or r2");
-		assert_eq!(format(
-			implies_right(or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]))),
-			"p1 or q1 or r1 -> p2 or q2 or r2");
-		assert_eq!(format(
-			implies_right(if_and_only_if(vec![or(p1q1r1())]),
-				if_and_only_if(vec![or(p2q2r2())]))),
-			"p1 or q1 or r1 -> p2 or q2 or r2");
-		assert_eq!(format(
-			implies_left(or(p1q1r1()), or(p2q2r2()))),
-			"p2 or q2 or r2 <- p1 or q1 or r1");
-		assert_eq!(format(
-			implies_left(and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]))),
-			"p2 or q2 or r2 <- p1 or q1 or r1");
-		assert_eq!(format(
-			implies_left(or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]))),
-			"p2 or q2 or r2 <- p1 or q1 or r1");
-		assert_eq!(format(
-			implies_left(if_and_only_if(vec![or(p1q1r1())]), if_and_only_if(vec![or(p2q2r2())]))),
+		assert_all!(i, implies_left(i(or(p1q1r1())), i(or(p2q2r2()))),
 			"p2 or q2 or r2 <- p1 or q1 or r1");
 
 		// Or + if and only if
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![p()]), if_and_only_if(vec![q()]),
-				if_and_only_if(vec![r()])])),
+		assert_all!(i, or(vec![i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()])),
+			i(if_and_only_if(vec![r()]))]),
 			"p or q or r");
-		assert_eq!(format(
-			or(vec![and(vec![if_and_only_if(vec![p()])]), and(vec![if_and_only_if(vec![q()])]),
-				and(vec![if_and_only_if(vec![r()])])])),
-			"p or q or r");
-		assert_eq!(format(
-			or(vec![or(vec![if_and_only_if(vec![p()])]), or(vec![if_and_only_if(vec![q()])]),
-				or(vec![if_and_only_if(vec![r()])])])),
-			"p or q or r");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![if_and_only_if(vec![p()])]),
-				if_and_only_if(vec![if_and_only_if(vec![q()])]),
-				if_and_only_if(vec![if_and_only_if(vec![r()])])])),
-			"p or q or r");
-		assert_eq!(format(
-			or(vec![if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()),
-				if_and_only_if(p3q3r3())])),
-			"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
-		assert_eq!(format(
-			or(vec![and(vec![if_and_only_if(p1q1r1())]), and(vec![if_and_only_if(p2q2r2())]),
-				and(vec![if_and_only_if(p3q3r3())])])),
-			"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
-		assert_eq!(format(
-			or(vec![or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]),
-				or(vec![if_and_only_if(p3q3r3())])])),
-			"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
-		assert_eq!(format(
-			or(vec![if_and_only_if(vec![if_and_only_if(p1q1r1())]),
-				if_and_only_if(vec![if_and_only_if(p2q2r2())]),
-				if_and_only_if(vec![if_and_only_if(p3q3r3())])])),
+		assert_all!(i, or(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())),
+			i(if_and_only_if(p3q3r3()))]),
 			"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
 
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![p()]), or(vec![q()]), or(vec![r()])])),
+		assert_all!(i, if_and_only_if(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]),
 			"p <-> q <-> r");
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![or(vec![p()])]), and(vec![or(vec![q()])]),
-				and(vec![or(vec![r()])])])),
-			"p <-> q <-> r");
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![or(vec![p()])]), or(vec![or(vec![q()])]),
-				or(vec![or(vec![r()])])])),
-			"p <-> q <-> r");
-		assert_eq!(format(
-			if_and_only_if(vec![if_and_only_if(vec![or(vec![p()])]),
-				if_and_only_if(vec![or(vec![q()])]), if_and_only_if(vec![or(vec![r()])])])),
-			"p <-> q <-> r");
-		assert_eq!(format(
-			if_and_only_if(vec![or(p1q1r1()), or(p2q2r2()), or(p3q3r3())])),
-			"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]),
-				and(vec![or(p3q3r3())])])),
-			"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]),
-				or(vec![or(p3q3r3())])])),
-			"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
-		assert_eq!(format(
-			if_and_only_if(vec![if_and_only_if(vec![or(p1q1r1())]),
-				if_and_only_if(vec![or(p2q2r2())]), if_and_only_if(vec![or(p3q3r3())])])),
+		assert_all!(i, if_and_only_if(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]),
 			"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
 	}
 
@@ -1635,124 +1110,25 @@ mod tests
 	fn format_combination_implies_and_lower()
 	{
 		// Implies + implies
-		assert_eq!(format(
-			implies_right(implies_right(p1(), q1()), implies_right(p2(), q2()))),
+		assert_all!(i, implies_right(i(implies_right(p1(), q1())), i(implies_right(p2(), q2()))),
 			"(p1 -> q1) -> p2 -> q2");
-		assert_eq!(format(
-			implies_right(and(vec![implies_right(p1(), q1())]),
-				and(vec![implies_right(p2(), q2())]))),
-			"(p1 -> q1) -> p2 -> q2");
-		assert_eq!(format(
-			implies_right(or(vec![implies_right(p1(), q1())]),
-				or(vec![implies_right(p2(), q2())]))),
-			"(p1 -> q1) -> p2 -> q2");
-		assert_eq!(format(
-			implies_right(if_and_only_if(vec![implies_right(p1(), q1())]),
-				if_and_only_if(vec![implies_right(p2(), q2())]))),
-			"(p1 -> q1) -> p2 -> q2");
-		assert_eq!(format(
-			implies_right(implies_left(p1(), q1()), implies_left(p2(), q2()))),
+		assert_all!(i, implies_right(i(implies_left(p1(), q1())), i(implies_left(p2(), q2()))),
 			"(q1 <- p1) -> (q2 <- p2)");
-		assert_eq!(format(
-			implies_right(and(vec![implies_left(p1(), q1())]),
-				and(vec![implies_left(p2(), q2())]))),
-			"(q1 <- p1) -> (q2 <- p2)");
-		assert_eq!(format(
-			implies_right(or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]))),
-			"(q1 <- p1) -> (q2 <- p2)");
-		assert_eq!(format(
-			implies_right(if_and_only_if(vec![implies_left(p1(), q1())]),
-				if_and_only_if(vec![implies_left(p2(), q2())]))),
-			"(q1 <- p1) -> (q2 <- p2)");
-		assert_eq!(format(
-			implies_left(implies_right(p1(), q1()), implies_right(p2(), q2()))),
+		assert_all!(i, implies_left(i(implies_right(p1(), q1())), i(implies_right(p2(), q2()))),
 			"(p2 -> q2) <- (p1 -> q1)");
-		assert_eq!(format(
-			implies_left(and(vec![implies_right(p1(), q1())]),
-				and(vec![implies_right(p2(), q2())]))),
-			"(p2 -> q2) <- (p1 -> q1)");
-		assert_eq!(format(
-			implies_left(or(vec![implies_right(p1(), q1())]), or(vec![implies_right(p2(), q2())]))),
-			"(p2 -> q2) <- (p1 -> q1)");
-		assert_eq!(format(
-			implies_left(if_and_only_if(vec![implies_right(p1(), q1())]),
-				if_and_only_if(vec![implies_right(p2(), q2())]))),
-			"(p2 -> q2) <- (p1 -> q1)");
-		assert_eq!(format(
-			implies_left(implies_left(p1(), q1()), implies_left(p2(), q2()))),
-			"q2 <- p2 <- (q1 <- p1)");
-		assert_eq!(format(
-			implies_left(and(vec![implies_left(p1(), q1())]), and(vec![implies_left(p2(), q2())]))),
-			"q2 <- p2 <- (q1 <- p1)");
-		assert_eq!(format(
-			implies_left(or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]))),
-			"q2 <- p2 <- (q1 <- p1)");
-		assert_eq!(format(
-			implies_left(if_and_only_if(vec![implies_left(p1(), q1())]),
-				if_and_only_if(vec![implies_left(p2(), q2())]))),
+		assert_all!(i, implies_left(i(implies_left(p1(), q1())), i(implies_left(p2(), q2()))),
 			"q2 <- p2 <- (q1 <- p1)");
 
 		// Implies + if and only if
-		assert_eq!(format(
-			implies_right(if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()))),
+		assert_all!(i, implies_right(i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2()))),
 			"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
-		assert_eq!(format(
-			implies_right(and(vec![if_and_only_if(p1q1r1())]),
-				and(vec![if_and_only_if(p2q2r2())]))),
-			"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
-		assert_eq!(format(
-			implies_right(or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]))),
-			"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
-		assert_eq!(format(
-			implies_right(if_and_only_if(vec![if_and_only_if(p1q1r1())]),
-				if_and_only_if(vec![if_and_only_if(p2q2r2())]))),
-			"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
-		assert_eq!(format(
-			implies_left(if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()))),
+		assert_all!(i, implies_left(i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2()))),
 			"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
-		assert_eq!(format(
-			implies_left(and(vec![if_and_only_if(p1q1r1())]), and(vec![if_and_only_if(p2q2r2())]))),
-			"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
-		assert_eq!(format(
-			implies_left(or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]))),
-			"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
-		assert_eq!(format(
-			implies_left(if_and_only_if(vec![if_and_only_if(p1q1r1())]),
-				if_and_only_if(vec![if_and_only_if(p2q2r2())]))),
-			"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
-		assert_eq!(format(
-			if_and_only_if(vec![implies_right(p1(), q1()), implies_right(p2(), q2()),
-				implies_right(p3(), q3())])),
+		assert_all!(i, if_and_only_if(vec![i(implies_right(p1(), q1())),
+			i(implies_right(p2(), q2())), i(implies_right(p3(), q3()))]),
 			"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![implies_right(p1(), q1())]),
-				and(vec![implies_right(p2(), q2())]), and(vec![implies_right(p3(), q3())])])),
-			"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![implies_right(p1(), q1())]),
-				or(vec![implies_right(p2(), q2())]), or(vec![implies_right(p3(), q3())])])),
-			"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
-		assert_eq!(format(
-			if_and_only_if(vec![if_and_only_if(vec![implies_right(p1(), q1())]),
-				if_and_only_if(vec![implies_right(p2(), q2())]),
-				if_and_only_if(vec![implies_right(p3(), q3())])])),
-			"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
-		assert_eq!(format(
-			if_and_only_if(vec![implies_left(p1(), q1()), implies_left(p2(), q2()),
-				implies_left(p3(), q3())])),
-			"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
-		assert_eq!(format(
-			if_and_only_if(vec![and(vec![implies_left(p1(), q1())]),
-				and(vec![implies_left(p2(), q2())]), and(vec![implies_left(p3(), q3())])])),
-			"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
-		assert_eq!(format(
-			if_and_only_if(vec![or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]),
-				or(vec![implies_left(p3(), q3())])])),
-			"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
-		assert_eq!(format(
-			if_and_only_if(vec![if_and_only_if(vec![implies_left(p1(), q1())]),
-				if_and_only_if(vec![implies_left(p2(), q2())]),
-				if_and_only_if(vec![implies_left(p3(), q3())])])),
+		assert_all!(i, if_and_only_if(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())),
+			i(implies_left(p3(), q3()))]),
 			"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
 	}
 }