diff --git a/src/convenience/mod.rs b/src/convenience/mod.rs
new file mode 100644
index 00000000..4fa2c769
--- /dev/null
+++ b/src/convenience/mod.rs
@@ -0,0 +1 @@
+pub mod unbox;
diff --git a/src/convenience/unbox/fol.rs b/src/convenience/unbox/fol.rs
new file mode 100644
index 00000000..db70cb51
--- /dev/null
+++ b/src/convenience/unbox/fol.rs
@@ -0,0 +1,51 @@
+use crate::syntax_tree::fol::{
+    AtomicFormula, BinaryConnective, Formula, Quantification, UnaryConnective,
+};
+
+pub enum UnboxedFormula {
+    AtomicFormula(AtomicFormula),
+    UnaryFormula {
+        connective: UnaryConnective,
+        formula: Formula,
+    },
+    BinaryFormula {
+        connective: BinaryConnective,
+        lhs: Formula,
+        rhs: Formula,
+    },
+    QuantifiedFormula {
+        quantification: Quantification,
+        formula: Formula,
+    },
+}
+
+impl UnboxedFormula {
+    pub fn rebox(self) -> Formula {
+        match self {
+            Self::AtomicFormula(f) => Formula::AtomicFormula(f),
+            Self::UnaryFormula {
+                connective,
+                formula,
+            } => Formula::UnaryFormula {
+                connective,
+                formula: Box::new(formula),
+            },
+            Self::BinaryFormula {
+                connective,
+                lhs,
+                rhs,
+            } => Formula::BinaryFormula {
+                connective,
+                lhs: Box::new(lhs),
+                rhs: Box::new(rhs),
+            },
+            Self::QuantifiedFormula {
+                quantification,
+                formula,
+            } => Formula::QuantifiedFormula {
+                quantification,
+                formula: Box::new(formula),
+            },
+        }
+    }
+}
diff --git a/src/convenience/unbox/mod.rs b/src/convenience/unbox/mod.rs
new file mode 100644
index 00000000..cc2c3c6b
--- /dev/null
+++ b/src/convenience/unbox/mod.rs
@@ -0,0 +1,44 @@
+use crate::syntax_tree::fol::Formula;
+
+use self::fol::UnboxedFormula;
+
+pub mod fol;
+
+pub trait Unbox {
+    type Unboxed;
+
+    fn unbox(self) -> Self::Unboxed;
+}
+
+impl Unbox for Formula {
+    type Unboxed = UnboxedFormula;
+
+    fn unbox(self) -> UnboxedFormula {
+        match self {
+            Self::AtomicFormula(f) => UnboxedFormula::AtomicFormula(f),
+            Self::UnaryFormula {
+                connective,
+                formula,
+            } => UnboxedFormula::UnaryFormula {
+                connective,
+                formula: *formula,
+            },
+            Self::BinaryFormula {
+                connective,
+                lhs,
+                rhs,
+            } => UnboxedFormula::BinaryFormula {
+                connective,
+                lhs: *lhs,
+                rhs: *rhs,
+            },
+            Self::QuantifiedFormula {
+                quantification,
+                formula,
+            } => UnboxedFormula::QuantifiedFormula {
+                quantification,
+                formula: *formula,
+            },
+        }
+    }
+}
diff --git a/src/main.rs b/src/main.rs
index 8c515fa9..800eca80 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,3 +1,4 @@
+pub mod convenience;
 pub mod formatting;
 pub mod parsing;
 pub mod simplifying;
diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs
index 8073903f..2f48be4d 100644
--- a/src/simplifying/fol/ht.rs
+++ b/src/simplifying/fol/ht.rs
@@ -1,4 +1,7 @@
-use crate::syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, UnboxedFormula};
+use crate::{
+    convenience::unbox::{fol::UnboxedFormula, Unbox as _},
+    syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula},
+};
 
 pub fn simplify(formula: Formula) -> Formula {
     simplify_outer(match formula {
diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs
index d9c7dadd..dc805d41 100644
--- a/src/syntax_tree/fol.rs
+++ b/src/syntax_tree/fol.rs
@@ -259,83 +259,6 @@ impl Formula {
             Formula::QuantifiedFormula { formula, .. } => formula.variables(),
         }
     }
-
-    pub fn unbox(self) -> UnboxedFormula {
-        match self {
-            Self::AtomicFormula(f) => UnboxedFormula::AtomicFormula(f),
-            Self::UnaryFormula {
-                connective,
-                formula,
-            } => UnboxedFormula::UnaryFormula {
-                connective,
-                formula: *formula,
-            },
-            Self::BinaryFormula {
-                connective,
-                lhs,
-                rhs,
-            } => UnboxedFormula::BinaryFormula {
-                connective,
-                lhs: *lhs,
-                rhs: *rhs,
-            },
-            Self::QuantifiedFormula {
-                quantification,
-                formula,
-            } => UnboxedFormula::QuantifiedFormula {
-                quantification,
-                formula: *formula,
-            },
-        }
-    }
-}
-
-pub enum UnboxedFormula {
-    AtomicFormula(AtomicFormula),
-    UnaryFormula {
-        connective: UnaryConnective,
-        formula: Formula,
-    },
-    BinaryFormula {
-        connective: BinaryConnective,
-        lhs: Formula,
-        rhs: Formula,
-    },
-    QuantifiedFormula {
-        quantification: Quantification,
-        formula: Formula,
-    },
-}
-
-impl UnboxedFormula {
-    pub fn rebox(self) -> Formula {
-        match self {
-            Self::AtomicFormula(f) => Formula::AtomicFormula(f),
-            Self::UnaryFormula {
-                connective,
-                formula,
-            } => Formula::UnaryFormula {
-                connective,
-                formula: Box::new(formula),
-            },
-            Self::BinaryFormula {
-                connective,
-                lhs,
-                rhs,
-            } => Formula::BinaryFormula {
-                connective,
-                lhs: Box::new(lhs),
-                rhs: Box::new(rhs),
-            },
-            Self::QuantifiedFormula {
-                quantification,
-                formula,
-            } => Formula::QuantifiedFormula {
-                quantification,
-                formula: Box::new(formula),
-            },
-        }
-    }
 }
 
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]