diff --git a/res/examples/external_equivalence/division/division.lp b/res/examples/external_equivalence/division/division.lp
new file mode 100644
index 00000000..7cb29a77
--- /dev/null
+++ b/res/examples/external_equivalence/division/division.lp
@@ -0,0 +1 @@
+div(N,D,Q,R) :- N = D*Q+R, 0 <= R, R < D.
diff --git a/res/examples/external_equivalence/division/division.po b/res/examples/external_equivalence/division/division.po
new file mode 100644
index 00000000..a84395d9
--- /dev/null
+++ b/res/examples/external_equivalence/division/division.po
@@ -0,0 +1,8 @@
+lemma:
+div(N$,D$,Q$,R$) and R$ < D$-1 -> div(N$+1,D$,Q$,R$+1).
+
+lemma:
+div(N$,D$,Q$,D$-1) -> div(N$+1,D$,Q$+1,0).
+
+inductive-lemma:
+forall N$ (N$ >= 0 -> (D$ > 0 -> exists Q$ R$ div(N$,D$,Q$,R$))).
diff --git a/res/examples/external_equivalence/division/division.spec b/res/examples/external_equivalence/division/division.spec
new file mode 100644
index 00000000..32d2d17f
--- /dev/null
+++ b/res/examples/external_equivalence/division/division.spec
@@ -0,0 +1 @@
+spec: forall N$ D$ (N$ >= 0 and D$ > 0 -> exists Q$ R$ div(N$,D$,Q$,R$)).
diff --git a/res/examples/external_equivalence/division/division.ug b/res/examples/external_equivalence/division/division.ug
new file mode 100644
index 00000000..156ba3d5
--- /dev/null
+++ b/res/examples/external_equivalence/division/division.ug
@@ -0,0 +1 @@
+output: div/4.
diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs
index 45a03f3f..31207bcc 100644
--- a/src/simplifying/fol/ht.rs
+++ b/src/simplifying/fol/ht.rs
@@ -112,7 +112,7 @@ fn remove_idempotences(formula: Formula) -> Formula {
     }
 }
 
-fn join_nested_quantifiers(formula: Formula) -> Formula {
+pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula {
     // Remove nested quantifiers
     // e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y)
 
diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs
index dcbf8019..c501ecbd 100644
--- a/src/syntax_tree/fol.rs
+++ b/src/syntax_tree/fol.rs
@@ -11,6 +11,7 @@ use {
             TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, UserGuideEntryParser,
             UserGuideParser, VariableParser,
         },
+        simplifying::fol::ht::join_nested_quantifiers,
         syntax_tree::{impl_node, Node},
         verifying::problem,
     },
@@ -819,6 +820,10 @@ impl Formula {
         self.quantify(Quantifier::Forall, variables)
     }
 
+    pub fn universal_closure_with_quantifier_joining(self) -> Formula {
+        join_nested_quantifiers(self.universal_closure())
+    }
+
     pub fn rename_conflicting_symbols(self, possible_conflicts: &IndexSet<Predicate>) -> Formula {
         match self {
             Formula::AtomicFormula(a) => {
@@ -944,6 +949,18 @@ impl AnnotatedFormula {
         }
     }
 
+    pub fn universal_closure_with_quantifier_joining(&self) -> Self {
+        AnnotatedFormula {
+            role: self.role,
+            direction: self.direction,
+            name: self.name.clone(),
+            formula: self
+                .formula
+                .clone()
+                .universal_closure_with_quantifier_joining(),
+        }
+    }
+
     pub fn replace_placeholders(mut self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
         self.formula = self.formula.replace_placeholders(mapping);
         self
diff --git a/src/verifying/outline/mod.rs b/src/verifying/outline/mod.rs
index e63ef901..5f7e1a89 100644
--- a/src/verifying/outline/mod.rs
+++ b/src/verifying/outline/mod.rs
@@ -337,7 +337,7 @@ impl ProofOutline {
             match anf.role {
                 fol::Role::Lemma | fol::Role::InductiveLemma => {
                     let general_lemma: GeneralLemma = anf
-                        .universal_closure()
+                        .universal_closure_with_quantifier_joining()
                         .replace_placeholders(placeholders)
                         .try_into()?;
                     match anf.direction {