diff --git a/aris/src/expr.rs b/aris/src/expr.rs
index eb0b398e..2a067906 100644
--- a/aris/src/expr.rs
+++ b/aris/src/expr.rs
@@ -1444,50 +1444,67 @@ impl Expr {
             let body = Box::new(Expr::Impl { left, right });
             (Expr::Quant { kind, name, body }, true)
         };
-        self.transform(&|expr| {
+        let prenex_step = |expr: Expr| -> (Expr, bool) {
             match expr {
                 Expr::Assoc { op, exprs } => match op {
-                    Op::And => transform_7ab(Op::And, exprs),
-                    Op::Or => transform_7ab(Op::Or, exprs),
+                    Op::And | Op::Or => transform_7ab(op, exprs),
                     _ => (Expr::Assoc { op, exprs }, false),
                 },
+
                 Expr::Impl { mut left, mut right } => {
                     let left_free = free_vars(&left);
                     let right_free = free_vars(&right);
+
+                    // 7c: Quant on left and not captured on right → flip
                     left = match *left {
-                        Expr::Quant { kind, name, body } if !right_free.contains(&name) => {
-                            // 7c case, quantifier is flipped
-                            match kind {
-                                QuantKind::Forall => {
-                                    return reconstruct_7cd(QuantKind::Exists, name, body, right);
-                                }
-                                QuantKind::Exists => {
-                                    return reconstruct_7cd(QuantKind::Forall, name, body, right);
-                                }
-                            }
-                        }
-                        left => Box::new(left),
+                        Expr::Quant { kind, name, body } if !right_free.contains(&name) => match kind {
+                            QuantKind::Forall => return reconstruct_7cd(QuantKind::Exists, name, body, right),
+                            QuantKind::Exists => return reconstruct_7cd(QuantKind::Forall, name, body, right),
+                        },
+                        other => Box::new(other),
                     };
+
+                    // 7d: Quant on right and not captured on left → no flip
                     right = match *right {
-                        Expr::Quant { kind, name, body } if !left_free.contains(&name) => {
-                            // 7d case, quantifier is not flipped
-                            // exhaustive match despite the bodies being the same: since if more quantifiers are added, should reconsider here instead of blindly hoisting the new quantifier
-                            match kind {
-                                QuantKind::Forall => {
-                                    return reconstruct_7cd(QuantKind::Forall, name, left, body);
-                                }
-                                QuantKind::Exists => {
-                                    return reconstruct_7cd(QuantKind::Exists, name, left, body);
-                                }
-                            }
-                        }
-                        right => Box::new(right),
+                        Expr::Quant { kind, name, body } if !left_free.contains(&name) => match kind {
+                            QuantKind::Forall => return reconstruct_7cd(QuantKind::Forall, name, left, body),
+                            QuantKind::Exists => return reconstruct_7cd(QuantKind::Exists, name, left, body),
+                        },
+                        other => Box::new(other),
                     };
+
+                    // if neither side hoisted, leave the implication intact
                     (Expr::Impl { left, right }, false)
                 }
-                _ => (expr, false),
+
+                // everything else is a no‑op
+                other => (other, false),
             }
-        })
+        };
+
+        // 1) do *all* possible one‑step hoists
+        let expr = self.transform(&prenex_step);
+
+        // 2) now peel off the entire quantifier prefix
+        let mut prefix = Vec::new();
+        let mut body = expr;
+        while let Expr::Quant { kind, name, body: inner } = body {
+            prefix.push((kind, name));
+            body = *inner;
+        }
+
+        // 3) stable‑sort so ∀s come before ∃s (same‐kind keep their relative order)
+        prefix.sort_by_key(|(kind, _)| match kind {
+            QuantKind::Forall => 0,
+            QuantKind::Exists => 1,
+        });
+
+        // 4) rebuild in reverse (so the first in `prefix` is the outermost)
+        let mut result = body;
+        for (kind, name) in prefix.into_iter().rev() {
+            result = Expr::Quant { kind, name, body: Box::new(result) };
+        }
+        result
     }
 
     /// ¬∀x (φ(x) → ψ(x)) ⇔ ∃x (φ(x) ∧ ¬ψ(x))
diff --git a/aris/src/proofs/proof_tests.rs b/aris/src/proofs/proof_tests.rs
index 20fa7b6d..ba1beb90 100644
--- a/aris/src/proofs/proof_tests.rs
+++ b/aris/src/proofs/proof_tests.rs
@@ -75,6 +75,7 @@ macro_rules! enumerate_subproofless_tests {
             test_bicon_elim, test_bicon_elim_negation, test_exclusion,
             test_excluded_middle, test_weak_induction, test_strong_induction,
             test_bicon_contraposition, test_biconditionalsubstitution,
+            test_prenex_basic, test_prenex_full,
         }
     };
 }
@@ -1512,3 +1513,89 @@ pub fn test_biconditionalsubstitution<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRe
     // Return proof and categorized results
     (prf, vec![i(r4), i(r5)], vec![i(r6), i(r7), i(r8)])
 }
+
+pub fn test_prenex_basic<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
+    use self::coproduct_inject as i;
+    use crate::parser::parse_unwrap as p;
+    let mut prf = P::new();
+
+    let p1 = prf.add_premise(p("forall x (P(x) & Q)"));
+    let p2 = prf.add_premise(p("exists x (P(x) & Q)"));
+    let p3 = prf.add_premise(p("forall x (P(x) | Q)"));
+    let p4 = prf.add_premise(p("exists x (P(x) | Q)"));
+    let p5 = prf.add_premise(p("forall x (P(x) -> Q)"));
+    let p6 = prf.add_premise(p("exists x (P(x) -> Q)"));
+    let p7 = prf.add_premise(p("forall x (Q -> P(x))"));
+    let p8 = prf.add_premise(p("exists x (Q -> P(x))"));
+
+    let r1 = prf.add_step(Justification(p("(forall x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
+    let r2 = prf.add_step(Justification(p("(exists x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p2.clone())], vec![]));
+    let r3 = prf.add_step(Justification(p("(forall x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p3.clone())], vec![]));
+    let r4 = prf.add_step(Justification(p("(exists x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p4.clone())], vec![]));
+    let r5 = prf.add_step(Justification(p("(exists x P(x)) -> Q"), RuleM::PrenexLaws, vec![i(p5.clone())], vec![]));
+    let r6 = prf.add_step(Justification(p("(forall x P(x)) -> Q"), RuleM::PrenexLaws, vec![i(p6.clone())], vec![]));
+    let r7 = prf.add_step(Justification(p("Q -> (forall x P(x))"), RuleM::PrenexLaws, vec![i(p7.clone())], vec![]));
+    let r8 = prf.add_step(Justification(p("Q -> (exists x P(x))"), RuleM::PrenexLaws, vec![i(p8.clone())], vec![]));
+
+    let r9 = prf.add_step(Justification(p("(exists x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
+    let r10 = prf.add_step(Justification(p("(forall x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
+    let r11 = prf.add_step(Justification(p("(forall x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p2.clone())], vec![]));
+    let r12 = prf.add_step(Justification(p("(exists x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p3.clone())], vec![]));
+    let r13 = prf.add_step(Justification(p("(forall x P(x)) | Q"), RuleM::PrenexLaws, vec![i(p4.clone())], vec![]));
+    let r14 = prf.add_step(Justification(p("(exists x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p5.clone())], vec![]));
+    let r15 = prf.add_step(Justification(p("(forall x P(x)) -> Q"), RuleM::PrenexLaws, vec![i(p5.clone())], vec![]));
+    let r16 = prf.add_step(Justification(p("(exists x P(x)) -> Q"), RuleM::PrenexLaws, vec![i(p6.clone())], vec![]));
+    let r17 = prf.add_step(Justification(p("Q -> (exists x P(x))"), RuleM::PrenexLaws, vec![i(p7.clone())], vec![]));
+    let r18 = prf.add_step(Justification(p("Q -> (forall x P(x))"), RuleM::PrenexLaws, vec![i(p8.clone())], vec![]));
+
+    (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r5), i(r6), i(r7), i(r8)], vec![i(r9), i(r10), i(r11), i(r12), i(r13), i(r14), i(r15), i(r16), i(r17), i(r18)])
+}
+
+pub fn test_prenex_full<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
+    use self::coproduct_inject as i;
+    use crate::parser::parse_unwrap as p;
+    let mut prf = P::new();
+
+    let p1 = prf.add_premise(p("exists x P(x) -> exists y Q(y)"));
+    let p2 = prf.add_premise(p("exists x (P(x) & exists y Q(y))"));
+    let p3 = prf.add_premise(p("forall x (P(x) | exists y Q(y))"));
+    let p4 = prf.add_premise(p("forall x (P(x) & exists x Q(x))"));
+    let p5 = prf.add_premise(p("exists y (P & Q & S(y))"));
+    let p6 = prf.add_premise(p("forall x (A(x) | B | C)"));
+    let p7 = prf.add_premise(p("exists x (P(x) & (Q | R))"));
+    let p8 = prf.add_premise(p("forall x (R | (P(x) -> Q))"));
+    let p9 = prf.add_premise(p("((exists x (P(x) & ~Q(x))) | (exists y R(y)))"));
+    let p10 = prf.add_premise(p("exists x (P(x) | forall y Q(y))"));
+    let p11 = prf.add_premise(p("exists x (P(x) -> exists y (Q(y) -> exists z R(z)))"));
+    let p15 = prf.add_premise(p("P & Q"));
+    let p16 = prf.add_premise(p("forall x P(x) & Q(x)"));
+    let p17 = prf.add_premise(p("exists x P(x) & exists x Q(x)"));
+    let p18 = prf.add_premise(p("forall x P(x) -> Q(x)"));
+    let p19 = prf.add_premise(p("exists y forall x R(x,y)"));
+
+    let r1 = prf.add_step(Justification(p("forall x (P(x) -> exists y Q(y))"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
+    let r2 = prf.add_step(Justification(p("exists y (exists x P(x) -> Q(y))"), RuleM::PrenexLaws, vec![i(p1.clone())], vec![]));
+    let r3 = prf.add_step(Justification(p("(exists x P(x)) & exists y Q(y)"), RuleM::PrenexLaws, vec![i(p2.clone())], vec![]));
+    let r4 = prf.add_step(Justification(p("exists x P(x) & exists y Q(y)"), RuleM::PrenexLaws, vec![i(p2.clone())], vec![]));
+    let r5 = prf.add_step(Justification(p("(forall x P(x)) | exists y Q(y)"), RuleM::PrenexLaws, vec![i(p3.clone())], vec![]));
+    let r6 = prf.add_step(Justification(p("forall x P(x) | exists y Q(y)"), RuleM::PrenexLaws, vec![i(p3.clone())], vec![]));
+    let r7 = prf.add_step(Justification(p("forall x (P(x) & exists x Q(x))"), RuleM::PrenexLaws, vec![i(p4.clone())], vec![]));
+    let r8 = prf.add_step(Justification(p("P & Q & exists y S(y)"), RuleM::PrenexLaws, vec![i(p5.clone())], vec![]));
+    let r9 = prf.add_step(Justification(p("(forall x A(x) | B | C)"), RuleM::PrenexLaws, vec![i(p6.clone())], vec![]));
+    let r10 = prf.add_step(Justification(p("(exists x P(x)) & (Q | R)"), RuleM::PrenexLaws, vec![i(p7.clone())], vec![]));
+    let r11 = prf.add_step(Justification(p("R | forall x (P(x) -> Q)"), RuleM::PrenexLaws, vec![i(p8.clone())], vec![]));
+    let r12 = prf.add_step(Justification(p("(exists x (exists y ((P(x) & ~Q(x)) | R(y))))"), RuleM::PrenexLaws, vec![i(p9.clone())], vec![]));
+    let r13 = prf.add_step(Justification(p("((exists x P(x)) | forall y Q(y))"), RuleM::PrenexLaws, vec![i(p10.clone())], vec![]));
+    let r14 = prf.add_step(Justification(p("((forall x P(x)) -> ((forall y Q(y)) -> exists z R(z)))"), RuleM::PrenexLaws, vec![i(p11.clone())], vec![]));
+    let r15 = prf.add_step(Justification(p("P & Q"), RuleM::PrenexLaws, vec![i(p15.clone())], vec![]));
+    let r16 = prf.add_step(Justification(p("forall x P(x) & Q(x)"), RuleM::PrenexLaws, vec![i(p16.clone())], vec![]));
+    let r17 = prf.add_step(Justification(p("exists x P(x) & exists x Q(x)"), RuleM::PrenexLaws, vec![i(p17.clone())], vec![]));
+    let r18 = prf.add_step(Justification(p("forall x P(x) -> Q(x)"), RuleM::PrenexLaws, vec![i(p18.clone())], vec![]));
+    let r19 = prf.add_step(Justification(p("forall x exists y R(x,y)"), RuleM::PrenexLaws, vec![i(p19.clone())], vec![]));
+
+    let e1 = prf.add_step(Justification(p("exists x (P & Q)"), RuleM::PrenexLaws, vec![i(p15.clone())], vec![]));
+    let e2 = prf.add_step(Justification(p("(forall x P(x)) & Q"), RuleM::PrenexLaws, vec![i(p16.clone())], vec![]));
+    let e3 = prf.add_step(Justification(p("forall x (P(x) -> Q(x))"), RuleM::PrenexLaws, vec![i(p18.clone())], vec![]));
+
+    (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r5), i(r6), i(r7), i(r8), i(r9), i(r10), i(r11), i(r12), i(r13), i(r14), i(r15), i(r16), i(r17), i(r18), i(r19)], vec![i(e1), i(e2), i(e3)])
+}