diff --git a/.github/actions/add-package/action.yml b/.github/actions/add-package/action.yml
index eeaaec3ee2e..0a82e3f4792 100644
--- a/.github/actions/add-package/action.yml
+++ b/.github/actions/add-package/action.yml
@@ -26,8 +26,9 @@ runs:
         # only work for the specific CI Python version.
         rm -rf ${{ inputs.build-dir }}/install/lib/python*
 
-        # Copy COPYING file to install directory
+        # Copy COPYING file and licenses directory to install directory
         cp COPYING ${{ inputs.build-dir }}/install/
+        cp -r licenses ${{ inputs.build-dir }}/install/
 
         # Create ZIP file
         pushd ${{ inputs.build-dir }}
diff --git a/.github/actions/package-python-wheel-macos/action.yml b/.github/actions/package-python-wheel-macos/action.yml
index 6850d142d73..78edc63b10a 100644
--- a/.github/actions/package-python-wheel-macos/action.yml
+++ b/.github/actions/package-python-wheel-macos/action.yml
@@ -10,7 +10,7 @@ inputs:
 runs:
   using: composite
   steps:
-    - uses: actions/setup-python@v4
+    - uses: actions/setup-python@v5
       if: runner.os == 'macOS'
       with:
         python-version: ${{ inputs.python-version }}
diff --git a/COPYING b/COPYING
index 9a040ad24a4..f589966a6d4 100644
--- a/COPYING
+++ b/COPYING
@@ -52,16 +52,23 @@ The following file contains third-party software.
 
 The copyright and licensing information of this file is in its header.
 
-cvc5 incorporates MiniSat code (see src/prop/minisat and src/prop/bvminisat),
-excluded from the above copyright.  See src/prop/minisat/LICENSE and
-src/prop/bvminisat/LICENSE for copyright and licensing information.
+cvc5 incorporates MiniSat code (see src/prop/minisat),
+excluded from the above copyright. See licenses/minisat-LICENSE
+for copyright and licensing information.
 
 cvc5 by default links against The GNU Multiple Precision (GMP) Arithmetic
-Library, which is licensed under GNU LGPL v3. See the file
+Library, which is licensed under GNU LGPL v3.  See the file
 licenses/lgpl-3.0.txt for a copy of that license.  Note that according to the
 terms of the LGPL, both cvc5's source, and the combined work (cvc5 linked with
 GMP) may (and do) remain under the more permissive modified BSD license.
 
+cvc5 also links against the CaDiCaL library
+(https://github.com/arminbiere/cadical), which is licensed under
+the MIT license.
+See https://raw.githubusercontent.com/arminbiere/cadical/master/LICENSE
+for copyright and licensing information.  Linking cvc5 against
+this library does not affect the license terms of the cvc5 code.
+
 The implementation of the floating point solver in cvc5 depends on symfpu
 (https://github.com/martin-cs/symfpu) written by Martin Brain.
 See https://raw.githubusercontent.com/martin-cs/symfpu/CVC4/LICENSE for
@@ -70,7 +77,6 @@ copyright and licensing information.
 cvc5 optionally links against the following libraries:
 
   ABC                (https://bitbucket.org/alanmi/abc)
-  CaDiCaL            (https://github.com/arminbiere/cadical)
   CryptoMiniSat      (https://github.com/msoos/cryptominisat)
   LibPoly            (https://github.com/SRI-CSL/libpoly)
   libedit            (https://thrysoee.dk/editline)
diff --git a/INSTALL.rst b/INSTALL.rst
index 46b8381bbdb..40ffa82dce3 100644
--- a/INSTALL.rst
+++ b/INSTALL.rst
@@ -118,13 +118,16 @@ versions; more recent versions should be compatible.
 - `GNU C and C++ (gcc and g++, >= 7) <https://gcc.gnu.org>`_
   or `Clang (>= 5) <https://clang.llvm.org>`_
 - `CMake >= 3.9 <https://cmake.org>`_
-- `Python >= 3.6 and <= 3.10 <https://www.python.org>`_
+- `Python >= 3.6 <https://www.python.org>`_
   + module `tomli <https://pypi.org/project/tomli/>`_
   + module `pyparsing <https://pypi.org/project/pyparsing/>`_
 - `GMP v6.3 (GNU Multi-Precision arithmetic library) <https://gmplib.org>`_
 - `CaDiCaL (SAT solver) <https://github.com/arminbiere/cadical>`_
 - `SymFPU <https://github.com/martin-cs/symfpu/tree/CVC4>`_
 
+For Python, to install these dependencies automatically, please use:
+
+  - `pip install -r contrib/requirements_build.txt`
 
 CaDiCaL (SAT solver)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -258,6 +261,10 @@ Dependencies for Language Bindings
   - `pytest <https://docs.pytest.org/en/6.2.x/>`_
   - The source for the `pythonic API <(https://github.com/cvc5/cvc5_pythonic_api)>`.
 
+For Python, to install these depedencies automatically, please use:
+
+  - `pip install -r contrib/requirements_python_dev.txt`
+
 If configured with ``--pythonic-path=PATH``, the build system will expect the Pythonic API's source to be at ``PATH``.
 Otherwise, if configured with ``--auto-download``, the build system will download it.
 
diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake
index f74be293a14..6a02a403ac1 100644
--- a/cmake/FindCLN.cmake
+++ b/cmake/FindCLN.cmake
@@ -44,7 +44,7 @@ if(NOT CLN_FOUND_SYSTEM)
   fail_if_cross_compiling("Windows" "" "CLN" "autoconf fails")
   fail_if_cross_compiling("" "arm" "CLN" "syntax error in configure")
 
-  set(CLN_VERSION "1.3.6")
+  set(CLN_VERSION "1.3.7")
   string(REPLACE "." "-" CLN_TAG ${CLN_VERSION})
 
   find_program(AUTORECONF autoreconf)
@@ -56,7 +56,7 @@ if(NOT CLN_FOUND_SYSTEM)
     CLN-EP
     ${COMMON_EP_CONFIG}
     URL "https://www.ginac.de/CLN/cln.git/?p=cln.git\\\;a=snapshot\\\;h=cln_${CLN_TAG}\\\;sf=tgz"
-    URL_HASH SHA1=71d02b90ef0575f06b7bafb8690f73e8064d8228
+    URL_HASH SHA1=bd6dec17cf1088bdd592794d9239d47c752cf3da
     DOWNLOAD_NAME cln.tgz
     CONFIGURE_COMMAND
       ${CMAKE_COMMAND} -E chdir <SOURCE_DIR> ./autogen.sh
diff --git a/contrib/get-alf-checker b/contrib/get-alf-checker
index c50dc4606d8..b452e3eb95c 100755
--- a/contrib/get-alf-checker
+++ b/contrib/get-alf-checker
@@ -24,7 +24,7 @@ ALFC_DIR="$BASE_DIR/alf-checker"
 mkdir -p $ALFC_DIR
 
 # download and unpack ALFC
-ALF_VERSION="b51d495b4871dc0c4e4f68e579a504cec288b022"
+ALF_VERSION="57b34b6b5c130eb44332149b110bed130b3281e3"
 download "https://github.com/cvc5/alfc/archive/$ALF_VERSION.tar.gz" $BASE_DIR/tmp/alfc.tgz
 tar --strip 1 -xzf $BASE_DIR/tmp/alfc.tgz -C $ALFC_DIR
 
diff --git a/contrib/packaging_python/mk_clean_wheel.sh b/contrib/packaging_python/mk_clean_wheel.sh
index 782a64b5eb5..27e13dcf4a0 100755
--- a/contrib/packaging_python/mk_clean_wheel.sh
+++ b/contrib/packaging_python/mk_clean_wheel.sh
@@ -40,7 +40,8 @@ source ./$ENVDIR/bin/activate
 
 # install packages
 pip install -q --upgrade pip setuptools auditwheel
-pip install -q Cython pytest tomli scikit-build flex pyparsing 
+pip install -r contrib/requirements_build.txt
+pip install -r contrib/requirements_python_dev.txt
 if [ "$(uname)" == "Darwin" ]; then
     # Mac version of auditwheel
     pip install -q delocate
@@ -59,6 +60,8 @@ rm -rf build_wheel/
 echo "Building pycvc5 wheel"
 
 pushd build_wheel
+# Copy the license files to be included in the wheel
+cmake --build . --target cvc5_python_licenses
 if [ -z "$PLATFORM" ] ; then
   python ../contrib/packaging_python/mk_wheel.py bdist_wheel -d dist
 else
diff --git a/contrib/packaging_python/mk_wheel.py b/contrib/packaging_python/mk_wheel.py
index 297cca98df4..e343194702f 100644
--- a/contrib/packaging_python/mk_wheel.py
+++ b/contrib/packaging_python/mk_wheel.py
@@ -113,9 +113,13 @@ def build_extension(self, ext):
     version=get_cvc5_version(),
     long_description='Python bindings for cvc5',
     url='https://github.com/cvc5/cvc5',
-    license='BSD-3-Clause',
+    license = "BSD-3-Clause AND LGPL-3.0-or-later AND MIT",
+    # BSD-3-Clause      : cvc5 library and Python API
+    # LGPL-3.0-or-later : LibPoly and GMP
+    # MIT               : Pythonic API
     zip_safe=False,
     ext_modules=[CMakeExtension('cvc5')],
     cmdclass=dict(build_ext=CMakeBuild),
-    tests_require=['pytest']
+    tests_require=['pytest'],
+    license_files = ['COPYING', 'licenses/*'],
 )
diff --git a/contrib/requirements_build.txt b/contrib/requirements_build.txt
new file mode 100644
index 00000000000..b1d0a9aa1d1
--- /dev/null
+++ b/contrib/requirements_build.txt
@@ -0,0 +1,2 @@
+tomli
+pyparsing
diff --git a/contrib/requirements_python_dev.txt b/contrib/requirements_python_dev.txt
new file mode 100644
index 00000000000..125abe538fd
--- /dev/null
+++ b/contrib/requirements_python_dev.txt
@@ -0,0 +1,3 @@
+Cython
+pytest
+scikit-build
diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst
index 0f020d03368..4efc645c387 100644
--- a/docs/api/python/python.rst
+++ b/docs/api/python/python.rst
@@ -47,7 +47,7 @@ Before building and installing, the following dependencies should be installed,
 .. code:: bash
 
   brew install cmake python gmp java
-  pip3 install cython tomli scikit-build pyparsing
+  pip3 install -r contrib/requirements_python_dev.txt
 
 
 Then `cvc5` can be installed from source as follows:
diff --git a/include/cvc5/cvc5.h b/include/cvc5/cvc5.h
index 2f7bc28bc6c..4a01e20e7fb 100644
--- a/include/cvc5/cvc5.h
+++ b/include/cvc5/cvc5.h
@@ -4642,11 +4642,15 @@ class CVC5_EXPORT Solver
    * @param format The proof format used to print the proof.  Must be
    * `modes::ProofFormat::NONE` if the proof is from a component other than
    * `modes::ProofComponent::FULL`.
+   * @param assertionNames Mapping between assertions and names, if they were
+   * given by the user.
    * @return The string representation of the proof in the given format.
    */
   std::string proofToString(
       Proof proof,
-      modes::ProofFormat format = modes::ProofFormat::DEFAULT) const;
+      modes::ProofFormat format = modes::ProofFormat::DEFAULT,
+      const std::map<cvc5::Term, std::string>& assertionNames =
+          std::map<cvc5::Term, std::string>()) const;
 
   /**
    * Get a list of learned literals that are entailed by the current set of
diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
index 89325a4404a..b14db21e761 100644
--- a/include/cvc5/cvc5_proof_rule.h
+++ b/include/cvc5/cvc5_proof_rule.h
@@ -1322,7 +1322,7 @@ enum ENUM(ProofRule) : uint32_t
    *
    * .. math::
    *
-   *   \inferruleSC{-\mid F, y_1=z_1,\dots, y_n=z_n}
+   *   \inferruleSC{-\mid F, (y_1 \ldots y_n), (z_1,\dots, z_n)}
    *   {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}}
    *   {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables}
    *
@@ -1395,21 +1395,29 @@ enum ENUM(ProofRule) : uint32_t
    * \mathit{index},b)` is null, in other words, neither is a prefix of the
    * other. Note it may be the case that one side of the equality denotes the
    * empty string.
+   * 
+   * This rule is used exclusively for strings.
    *
-   * Alternatively, if the equality is between sequences, this rule has the
-   * form:
+   * \endverbatim
+   */
+  EVALUE(CONCAT_CONFLICT),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Strings -- Core rules -- Concatenation conflict for disequal characters**
    *
    * .. math::
    *
    *   \inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \deq s_1 \mid b}{\bot}
    *
-   * where t_1 and s_1 are constants of length one, or otherwise one side
-   * of the equality is the empty sequence and t_1 or s_1 corresponding to
+   * where $t_1$ and $s_1$ are constants of length one, or otherwise one side
+   * of the equality is the empty sequence and $t_1$ or $s_1$ corresponding to
    * that side is the empty sequence.
+   * 
+   * This rule is used exclusively for sequences.
    *
    * \endverbatim
    */
-  EVALUE(CONCAT_CONFLICT),
+  EVALUE(CONCAT_CONFLICT_DEQ),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Strings -- Core rules -- Concatenation split**
@@ -1768,7 +1776,7 @@ enum ENUM(ProofRule) : uint32_t
    * **Arithmetic -- Trichotomy of the reals**
    *
    * .. math::
-   *   \inferrule{A, B \mid C}{C}
+   *   \inferrule{A, B \mid -}{C}
    *
    * where :math:`\neg A, \neg B, C` are :math:`x < c, x = c, x > c` in some order.
    * Note that :math:`\neg` here denotes arithmetic negation, i.e., flipping :math:`\geq` to :math:`<` etc.
diff --git a/licenses/antlr3-LICENSE b/licenses/antlr3-LICENSE
deleted file mode 100644
index 6364129f5ab..00000000000
--- a/licenses/antlr3-LICENSE
+++ /dev/null
@@ -1,28 +0,0 @@
-[The "BSD licence"]
-Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC
-http://www.temporal-wave.com
-http://www.linkedin.com/in/jimidle
-
-All rights reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions
-are met:
-1. Redistributions of source code must retain the above copyright
-   notice, this list of conditions and the following disclaimer.
-2. Redistributions in binary form must reproduce the above copyright
-   notice, this list of conditions and the following disclaimer in the
-   documentation and/or other materials provided with the distribution.
-3. The name of the author may not be used to endorse or promote products
-   derived from this software without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
-IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
-OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
-IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
-INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
-NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
-THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/licenses/minisat-LICENSE b/licenses/minisat-LICENSE
new file mode 100644
index 00000000000..22816ff39b1
--- /dev/null
+++ b/licenses/minisat-LICENSE
@@ -0,0 +1,21 @@
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+           Copyright (c) 2007-2010  Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a
+copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/proofs/alf/programs/Quantifiers.smt3 b/proofs/alf/programs/Quantifiers.smt3
index 415579e89fd..828f8b0855c 100644
--- a/proofs/alf/programs/Quantifiers.smt3
+++ b/proofs/alf/programs/Quantifiers.smt3
@@ -19,4 +19,3 @@
     ((substitute_list @list.nil @list.nil F)       F)
   )
 )
-
diff --git a/proofs/alf/rules/Booleans.smt3 b/proofs/alf/rules/Booleans.smt3
index bfa77afff70..44eedb46827 100644
--- a/proofs/alf/rules/Booleans.smt3
+++ b/proofs/alf/rules/Booleans.smt3
@@ -3,44 +3,6 @@
 
 (include "../programs/Nary.smt3")
 
-; SCOPE
-(declare-rule scope
-  ((F Bool) (G Bool))
-  :assumption F
-  :premises (G)
-  :args ()
-  :conclusion (=> F G)
-)
-
-; `extract_antec F C`
-; returns the antecedant of F up to C,
-; e.g. returns (and G1 G2) when F is (=> G1 (=> G2 C)).
-(program extract_antec
-   ((C Bool) (F1 Bool) (F2 Bool))
-   (Bool Bool) Bool
-   (
-   ((extract_antec C C) true)
-   ((extract_antec (=> F1 F2) C) (alf.cons and F1 (extract_antec F2 C)))
-   )
-)
-
-(program run_process_scope
-   ((C Bool) (F Bool))
-   (Bool Bool) Bool
-   (
-   ((run_process_scope F false) (not (alf.from_list and (extract_antec F false))))
-   ((run_process_scope F C) (=> (alf.from_list and (extract_antec F C)) C))
-   )
-)
-
-; this rule processes the result of n scopes into the conclusion expected by ProofRule::SCOPE
-(declare-rule process_scope
-  ((C Bool) (F Bool))
-  :premises (F)
-  :args (C)
-  :conclusion (run_process_scope F C)
-)
-
 ; SPLIT
 (declare-rule split ((F Bool))
     :args (F)
diff --git a/proofs/alf/rules/Builtin.smt3 b/proofs/alf/rules/Builtin.smt3
index 29e1006f828..d697958309d 100644
--- a/proofs/alf/rules/Builtin.smt3
+++ b/proofs/alf/rules/Builtin.smt3
@@ -1,5 +1,43 @@
 (include "../theories/Builtin.smt3")
 
+; SCOPE
+(declare-rule scope
+  ((F Bool) (G Bool))
+  :assumption F
+  :premises (G)
+  :args ()
+  :conclusion (=> F G)
+)
+
+; `extract_antec F C`
+; returns the antecedant of F up to C,
+; e.g. returns (and G1 G2) when F is (=> G1 (=> G2 C)).
+(program extract_antec
+   ((C Bool) (F1 Bool) (F2 Bool))
+   (Bool Bool) Bool
+   (
+   ((extract_antec C C) true)
+   ((extract_antec (=> F1 F2) C) (alf.cons and F1 (extract_antec F2 C)))
+   )
+)
+
+(program run_process_scope
+   ((C Bool) (F Bool))
+   (Bool Bool) Bool
+   (
+   ((run_process_scope F false) (not (alf.from_list and (extract_antec F false))))
+   ((run_process_scope F C) (=> (alf.from_list and (extract_antec F C)) C))
+   )
+)
+
+; this rule processes the result of n scopes into the conclusion expected by ProofRule::SCOPE
+(declare-rule process_scope
+  ((C Bool) (F Bool))
+  :premises (F)
+  :args (C)
+  :conclusion (run_process_scope F C)
+)
+
 (declare-rule remove_term_formula_axiom ((T Type) (b Bool) (t1 T) (t2 T))
   :args ((ite b t1 t2))
   :conclusion
diff --git a/proofs/alf/rules/Quantifiers.smt3 b/proofs/alf/rules/Quantifiers.smt3
index eaeee1698c3..89e5e99c1fb 100644
--- a/proofs/alf/rules/Quantifiers.smt3
+++ b/proofs/alf/rules/Quantifiers.smt3
@@ -34,8 +34,16 @@
       t
       (
         ; special case for witness
-        ((skolem (@k.QUANTIFIERS_SKOLEMIZE (exists (@list x) F) x)) (= t (witness x F)))
+        ((skolem (@k.QUANTIFIERS_SKOLEMIZE (exists (@list x) F) x)) (= t (witness (@list x) F)))
         ((skolem x)                                                 (= t x))
       )
    )
 )
+
+; B is the formula to apply to
+; vs is a list of variables to substitution for the variable list ts
+; Note we don't currently check whether this is valid renaming.
+(declare-rule alpha_equiv ((B Bool) (vs @List) (ts @List))
+  :args (B vs ts)
+  :conclusion (= B (substitute_list vs ts B))
+)
diff --git a/proofs/alf/rules/Uf.smt3 b/proofs/alf/rules/Uf.smt3
index 4374fbbe3ba..99f3f3a0bda 100644
--- a/proofs/alf/rules/Uf.smt3
+++ b/proofs/alf/rules/Uf.smt3
@@ -57,20 +57,27 @@
 )
 
 ; N-ary congruence
-; note that arguments are provided in reverse order to avoid intermediate node construction
-(program mk_nary_cong ((U Type) (f (-> U U)) (t1 U) (t2 U) (s1 U) (s2 U) (tail Bool :list))
-    ((-> U U) U U Bool) Bool
+; We use two side conditions for computing each side of the returned equality.
+; This avoids intermediate node construction.
+(program mk_nary_cong_lhs ((U Type) (f (-> U U)) (s1 U) (s2 U) (tail Bool :list))
+    ((-> U U) Bool) Bool
     (
-        ((mk_nary_cong f t1 t2 (and (= s1 s2) tail)) (mk_nary_cong f (f s1 t1) (f s2 t2) tail))
-        ((mk_nary_cong f t1 t2 true)                 (= t1 t2))
-        ((mk_nary_cong f t1 t2 (= s1 s2))            (= (f s1 t1) (f s2 t2)))
+        ((mk_nary_cong_lhs f (and (= s1 s2) tail)) (f s1 (mk_nary_cong_lhs f tail)))
+        ((mk_nary_cong_lhs f true)                 (alf.emptylist f))
+    )
+)
+(program mk_nary_cong_rhs ((U Type) (f (-> U U)) (s1 U) (s2 U) (tail Bool :list))
+    ((-> U U) Bool) Bool
+    (
+        ((mk_nary_cong_rhs f (and (= s1 s2) tail)) (f s2 (mk_nary_cong_rhs f tail)))
+        ((mk_nary_cong_rhs f true)                 (alf.emptylist f))
     )
 )
 
 (declare-rule nary_cong ((U Type) (E Bool) (f (-> U U)) (nil U))
     :premise-list E and
-    :args (f nil)
-    :conclusion (mk_nary_cong f nil nil E)
+    :args (f)
+    :conclusion (= (mk_nary_cong_lhs f E) (mk_nary_cong_rhs f E))
 )
 
 ; TRUE_INTRO
diff --git a/proofs/alf/theories/Builtin.smt3 b/proofs/alf/theories/Builtin.smt3
index 6b15589a1fc..0a5349916d6 100644
--- a/proofs/alf/theories/Builtin.smt3
+++ b/proofs/alf/theories/Builtin.smt3
@@ -22,7 +22,14 @@
    :chainable and
 )
 
-(declare-const lambda (-> (! Type :var A :implicit) (! Type :var B :implicit) A B (-> A B)))
+(program get_lambda_type ((x @List) (xs @List :list) (B Type))
+  (@List Type) Type
+  (
+    ((get_lambda_type (@list x xs) B) (-> (alf.typeof x) (get_lambda_type xs B)))
+    ((get_lambda_type @list.nil B)    B)
+  )
+)
+(declare-const lambda (-> (! Type :var B :implicit) (! @List :var L) B (get_lambda_type L B)) :binder @list)
 
 (declare-const distinct (-> (! Type :var A :implicit) A A Bool) :pairwise and)
 
diff --git a/proofs/alf/theories/Quantifiers.smt3 b/proofs/alf/theories/Quantifiers.smt3
index b7577e89bd8..10bbeffef91 100644
--- a/proofs/alf/theories/Quantifiers.smt3
+++ b/proofs/alf/theories/Quantifiers.smt3
@@ -4,7 +4,14 @@
 
 (declare-const exists (-> @List Bool Bool) :binder @list)
 
-(declare-const witness (-> (! Type :var T :implicit) T Bool T))
+; returns the type of the element in the list, if the list is a singleton.
+(program get_witness_type ((x @List))
+  (@List) Type
+  (
+    ((get_witness_type (@list x)) (alf.typeof x))
+  )
+)
+(declare-const witness (-> (! @List :var L) Bool (get_witness_type L)) :binder @list)
 
 ; skolems
 (declare-const @k.QUANTIFIERS_SKOLEMIZE (-> (! Type :var T :implicit) Bool T T))
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 49c1258357c..1b2217b185b 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7385,12 +7385,21 @@ std::vector<Proof> Solver::getProof(modes::ProofComponent c) const
   CVC5_API_TRY_CATCH_END;
 }
 
-std::string Solver::proofToString(Proof proof, modes::ProofFormat format) const
+std::string Solver::proofToString(
+    Proof proof,
+    modes::ProofFormat format,
+    const std::map<cvc5::Term, std::string>& assertionNames) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   std::ostringstream ss;
-  this->d_slv->printProof(ss, proof.getProofNode(), format);
+  // convert the map's domain to use nodes rather than terms
+  std::map<internal::Node, std::string> nodeAssertionNames;
+  for (const auto& p : assertionNames)
+  {
+    nodeAssertionNames[p.first.getNode()] = p.second;
+  }
+  this->d_slv->printProof(ss, proof.getProofNode(), format, nodeAssertionNames);
   return ss.str();
   ////////
   CVC5_API_TRY_CATCH_END;
diff --git a/src/api/cpp/cvc5_proof_rule.cpp b/src/api/cpp/cvc5_proof_rule.cpp
index 574018f9b11..95ba52a3dda 100644
--- a/src/api/cpp/cvc5_proof_rule.cpp
+++ b/src/api/cpp/cvc5_proof_rule.cpp
@@ -134,6 +134,7 @@ const char* toString(ProofRule id)
     case ProofRule::CONCAT_EQ: return "CONCAT_EQ";
     case ProofRule::CONCAT_UNIFY: return "CONCAT_UNIFY";
     case ProofRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT";
+    case ProofRule::CONCAT_CONFLICT_DEQ: return "CONCAT_CONFLICT_DEQ";
     case ProofRule::CONCAT_SPLIT: return "CONCAT_SPLIT";
     case ProofRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT";
     case ProofRule::CONCAT_LPROP: return "CONCAT_LPROP";
diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index 027d659859d..4e570a5e2a0 100644
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -178,7 +178,6 @@ python_extension_module(cvc5_python_base)
 find_package(CVC5PythonicAPI)
 
 set(COPIED_PYTHONIC_FILES
-  "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/LICENSE.txt"
   "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/__init__.py"
   "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/cvc5_pythonic.py"
   "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/cvc5_pythonic_printer.py"
@@ -191,11 +190,43 @@ add_custom_command(
     ${CMAKE_COMMAND} -E copy_directory
     "${CVC5PythonicAPI_BASEDIR}/cvc5_pythonic_api"
     "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic"
+  # Remove the license of the Pythonic API from the package's source files.
+  # The license file is included in the package's dist-info dir by setup()
+  COMMAND
+    ${CMAKE_COMMAND} -E remove
+    "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/LICENSE.txt"
   DEPENDS cvc5_python_base CVC5PythonicAPI
 )
 
 add_custom_target(cvc5_python_api ALL DEPENDS ${COPIED_PYTHONIC_FILES})
 
+set(LICENSE_FILES
+  "${CMAKE_BINARY_DIR}/COPYING"
+  "${CMAKE_BINARY_DIR}/licenses/lgpl-3.0.txt"
+  "${CMAKE_BINARY_DIR}/licenses/pythonic-LICENSE"
+)
+
+add_custom_command(
+  OUTPUT
+    ${LICENSE_FILES}
+  COMMAND
+    ${CMAKE_COMMAND} -E copy
+    "${PROJECT_SOURCE_DIR}/COPYING"
+    "${CMAKE_BINARY_DIR}/COPYING"
+  COMMAND
+    ${CMAKE_COMMAND} -E copy_directory
+    "${PROJECT_SOURCE_DIR}/licenses"
+    "${CMAKE_BINARY_DIR}/licenses"
+  COMMAND
+    ${CMAKE_COMMAND} -E copy
+    "${CVC5PythonicAPI_BASEDIR}/cvc5_pythonic_api/LICENSE.txt"
+    "${CMAKE_BINARY_DIR}/licenses/pythonic-LICENSE"
+  DEPENDS CVC5PythonicAPI
+)
+
+# Copy license files to build directory where setup() can find them
+add_custom_target(cvc5_python_licenses DEPENDS ${LICENSE_FILES})
+
 # Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html
 # Create a wrapper python directory and generate a distutils setup.py file
 configure_file(setup.py.in setup.py)
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index fcf57384a5c..6821430d94a 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1559,7 +1559,7 @@ cdef class Solver:
                 if a < 0 or a >= 2 ** 31:
                     raise ValueError(
                             "Argument {} must fit in a uint32_t".format(a))
-                v.push_back((<uint32_t?> a))
+                v.push_back(<uint32_t?> a)
             op.cop = self.csolver.mkOp(<c_Kind> k.value, v)
         return op
 
@@ -1618,7 +1618,7 @@ cdef class Solver:
                     <const string &> str(val).encode())
         else:
             assert(isinstance(val, int))
-            term.cterm = self.csolver.mkInteger((<int?> val))
+            term.cterm = self.csolver.mkInteger(<int?> val)
         return term
 
     def mkReal(self, numerator, denominator=None):
@@ -3103,7 +3103,7 @@ cdef class Solver:
                    free variables in :math:`y_1...y_n`
                  - If :math:`Q` is :math:`\\exists`, let :math:`(A \\wedge Q_n)`
                    be the formula
-                   :math:`(A \\wedge \\neg (\\phi \wedge Q_1) \\wedge ... \\wedge \\neg (\\phi \\wedge Q_n))`
+                   :math:`(A \\wedge \\neg (\\phi \\wedge Q_1) \\wedge ... \\wedge \\neg (\\phi \\wedge Q_n))`
                    where for each :math:`i = 1...n`, formula
                    :math:`(\\phi \\wedge Q_i)` is the result of calling
                    :py:meth:`getQuantifierEliminationDisjunct()`
@@ -4553,7 +4553,7 @@ cdef class Term:
         return (get0(t), get1(t), term)
 
     def isSetValue(self):
-        """
+        r"""
             A term is a set value if it is considered to be a (canonical)
             constant set value.  A canonical set value is one whose AST is:
 
diff --git a/src/api/python/genenums.py.in b/src/api/python/genenums.py.in
index efca44d0324..238c5afa8bc 100644
--- a/src/api/python/genenums.py.in
+++ b/src/api/python/genenums.py.in
@@ -71,15 +71,15 @@ comment_repls = [
     (':cpp:func:`(.*?)`', '\\1'),
     (':cpp:enumerator:`(.*?)`', ':py:obj:`\\1`'),
     # introduce proper python references
-    ('Term::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Term.\\1()`'),
-    ('Solver::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`Solver.\\1()`'),
-    ('Solver::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Solver.\\1()`'),
-    ('DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`DatatypeConstructor.\\1()`'),
-    ('DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`DatatypeConstructor.\\1()`'),
-    ('Datatype::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`Datatype.\\1()`'),
-    ('Datatype::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Datatype.\\1()`'),
-    ('DatatypeSelector::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`DatatypeSelector.\\1()`'),
-    ('DatatypeSelector::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`DatatypeSelector.\\1()`'),
+    (r'Term::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Term.\\1()`'),
+    (r'Solver::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`Solver.\\1()`'),
+    (r'Solver::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Solver.\\1()`'),
+    (r'DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`DatatypeConstructor.\\1()`'),
+    (r'DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`DatatypeConstructor.\\1()`'),
+    (r'Datatype::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`Datatype.\\1()`'),
+    (r'Datatype::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Datatype.\\1()`'),
+    (r'DatatypeSelector::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`DatatypeSelector.\\1()`'),
+    (r'DatatypeSelector::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`DatatypeSelector.\\1()`'),
     ('\\\\', '\\\\\\\\'),
 ]
 
diff --git a/src/base/collect_tags.py b/src/base/collect_tags.py
index 3534584ab13..ce0b27229ac 100644
--- a/src/base/collect_tags.py
+++ b/src/base/collect_tags.py
@@ -33,7 +33,7 @@ def parse_args():
     {
         'patterns' : ['assertions::pre-{}', 'assertions::post-{}'],
         'collector' : lambda basedir:
-            re.findall('registerPassInfo\("([a-z-]+)"',
+            re.findall(r'registerPassInfo\("([a-z-]+)"',
                 open(os.path.join(basedir, 'preprocessing', 'preprocessing_pass_registry.cpp')).read()
             )
     }
diff --git a/src/parser/commands.cpp b/src/parser/commands.cpp
index 11b8edb521d..a423170587e 100644
--- a/src/parser/commands.cpp
+++ b/src/parser/commands.cpp
@@ -1586,7 +1586,10 @@ void GetProofCommand::invoke(cvc5::Solver* solver, SymManager* sm)
       {
         ss << "(!" << std::endl;
       }
-      ss << solver->proofToString(p, format);
+      // get assertions, and build a map between them and their names
+      std::map<cvc5::Term, std::string> assertionNames =
+          sm->getExpressionNames(true);
+      ss << solver->proofToString(p, format, assertionNames);
       if (commentProves)
       {
         ss << ":proves " << p.getResult() << ")" << std::endl;
diff --git a/src/proof/alethe/alethe_printer.cpp b/src/proof/alethe/alethe_printer.cpp
index 657b0668519..335e11a810a 100644
--- a/src/proof/alethe/alethe_printer.cpp
+++ b/src/proof/alethe/alethe_printer.cpp
@@ -82,8 +82,10 @@ void AletheProofPrinter::printTerm(std::ostream& out, TNode n)
   out << ss.str();
 }
 
-void AletheProofPrinter::print(std::ostream& out,
-                               std::shared_ptr<ProofNode> pfn)
+void AletheProofPrinter::print(
+    std::ostream& out,
+    std::shared_ptr<ProofNode> pfn,
+    const std::map<Node, std::string>& assertionNames)
 {
   Trace("alethe-printer") << "- Print proof in Alethe format. " << std::endl;
   std::shared_ptr<ProofNode> innerPf = pfn->getChildren()[0];
@@ -119,11 +121,19 @@ void AletheProofPrinter::print(std::ostream& out,
   // Print assumptions and add them to the list but do not print anchor.
   for (size_t i = 3, size = args.size(); i < size; i++)
   {
-    // assumptions are always being declared
-    out << "(assume a" << i - 3 << " ";
+    auto it = assertionNames.find(args[i]);
+    if (it != assertionNames.end())
+    {
+      out << "(assume " << it->second << " ";
+      assumptions[args[i]] = it->second;
+    }
+    else
+    {  // assumptions are always being declared
+      out << "(assume a" << i - 3 << " ";
+      assumptions[args[i]] = "a" + std::to_string(i - 3);
+    }
     printTerm(out, args[i]);
     out << ")\n";
-    assumptions[args[i]] = "a" + std::to_string(i - 3);
   }
   // Then, print the rest of the proof node
   uint32_t start_t = 1;
diff --git a/src/proof/alethe/alethe_printer.h b/src/proof/alethe/alethe_printer.h
index f1cde85b852..791a9eff93f 100644
--- a/src/proof/alethe/alethe_printer.h
+++ b/src/proof/alethe/alethe_printer.h
@@ -69,8 +69,12 @@ class AletheProofPrinter : protected EnvObj
    *
    * @param out The stream to write to
    * @param pfn The proof node to be printed
+   * @param assertionNames Mapping between assertions and names, if they were
+   * given by the user.
    */
-  void print(std::ostream& out, std::shared_ptr<ProofNode> pfn);
+  void print(std::ostream& out,
+             std::shared_ptr<ProofNode> pfn,
+             const std::map<Node, std::string>& assertionNames);
 
  private:
   /** Used for printing the proof node after the initial Alethe anchor has been
diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp
index 7277199e76b..34f88bcac14 100644
--- a/src/proof/alf/alf_node_converter.cpp
+++ b/src/proof/alf/alf_node_converter.cpp
@@ -161,24 +161,6 @@ Node AlfNodeConverter::postConvert(Node n)
     ss << (r.sgn() == -1 ? "-" : "") << num << "/" << den;
     return mkInternalSymbol(ss.str(), tn);
   }
-  else if (k == Kind::LAMBDA || k == Kind::WITNESS)
-  {
-    // e.g. (lambda ((x1 T1) ... (xn Tk)) P) is
-    // (lambda x1 (lambda x2 ... (lambda xn P)))
-    Node ret = n[1];
-    TypeNode tnr = ret.getType();
-    std::stringstream opName;
-    opName << printer::smt2::Smt2Printer::smtKindString(k);
-    for (size_t i = 0, nchild = n[0].getNumChildren(); i < nchild; i++)
-    {
-      size_t ii = (nchild - 1) - i;
-      Node v = convert(n[0][ii]);
-      // use the body return type for all terms except the last one.
-      tnr = ii == 0 ? n.getType() : nm->mkFunctionType({v.getType()}, tnr);
-      ret = mkInternalApp(opName.str(), {v, ret}, tnr);
-    }
-    return ret;
-  }
   else if (n.isClosure())
   {
     // e.g. (forall ((x1 T1) ... (xn Tk)) P) is
diff --git a/src/proof/alf/alf_post_processor.cpp b/src/proof/alf/alf_post_processor.cpp
index 4fdfc9d0e27..307ad7a02b0 100644
--- a/src/proof/alf/alf_post_processor.cpp
+++ b/src/proof/alf/alf_post_processor.cpp
@@ -50,7 +50,6 @@ bool AlfProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
 {
   switch (pn->getRule())
   {
-    case ProofRule::SCOPE:
     case ProofRule::CONG:
     case ProofRule::CONCAT_CONFLICT:
     case ProofRule::SKOLEM_INTRO: return true;
@@ -98,35 +97,9 @@ bool AlfProofPostprocessCallback::update(Node res,
 {
   Trace("alf-proof") << "...Alf pre-update " << res << " " << id << " "
                      << children << " / " << args << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
 
   switch (id)
   {
-    case ProofRule::SCOPE:
-    {
-      // On the first two calls to update, the proof nodes are the outermost
-      // scopes of the proof. These scopes should not be printed in the AletheLF
-      // proof. Instead, the AletheLF proof printer will print the proper scopes
-      // around the proof, which e.g. involves an AletheLF "check" command.
-      if (d_numIgnoredScopes < 2)
-      {
-        d_numIgnoredScopes++;
-        // Note that we do not want to modify the top-most SCOPEs.
-        return false;
-      }
-      Node curr = children[0];
-      for (size_t i = 0, nargs = args.size(); i < nargs; i++)
-      {
-        size_t ii = (nargs - 1) - i;
-        Node next = nm->mkNode(Kind::IMPLIES, args[ii], curr);
-        addAlfStep(AlfRule::SCOPE, next, {curr}, {args[ii]}, *cdp);
-        curr = next;
-      }
-      // convert (=> F1 (=> ... (=> Fn C)...)) to (=> (and F1 ... Fn) C) or
-      // (not (and F1 ... Fn))
-      addAlfStep(AlfRule::PROCESS_SCOPE, res, {curr}, {children[0]}, *cdp);
-    }
-    break;
     case ProofRule::CONG:
     {
       Assert(res.getKind() == Kind::EQUAL);
@@ -148,30 +121,7 @@ bool AlfProofPostprocessCallback::update(Node res,
       Node op = d_tproc.getOperatorOfTerm(res[0]);
       Trace("alf-proof") << "Processing cong for op " << op << " "
                          << op.getType() << std::endl;
-      if (k == Kind::LAMBDA || k == Kind::WITNESS)
-      {
-        Assert(res[1].getKind() == k && res[0][0] == res[1][0]);
-        Node lam1 = d_tproc.convert(res[0]);
-        Node lam2 = d_tproc.convert(res[1]);
-        for (size_t i = 0, nvars = res[0][0].getNumChildren(); i < nvars; i++)
-        {
-          Assert(lam1.getNumChildren() == 2 && lam2.getNumChildren() == 2);
-          Node varEq = lam1[0].eqNode(lam1[0]);
-          cdp->addStep(varEq, ProofRule::REFL, {}, {lam1[0]});
-          Node bodyEq = i + 1 == nvars ? children[1] : lam1[1].eqNode(lam2[1]);
-          Node lamEq = lam1.eqNode(lam2);
-          Node conclusion = i == 0 ? res : lamEq;
-          addAlfStep(AlfRule::CONG,
-                     conclusion,
-                     {varEq, bodyEq},
-                     {lam1.getOperator()},
-                     *cdp);
-          lam1 = lam1[1];
-          lam2 = lam2[1];
-        }
-        return true;
-      }
-      else if (res[0].isClosure())
+      if (res[0].isClosure())
       {
         Assert(children.size() >= 2);
         // variable lists should be equal
@@ -208,13 +158,8 @@ bool AlfProofPostprocessCallback::update(Node res,
       }
       if (isNary)
       {
-        std::vector<Node> rchildren = children;
-        std::reverse(rchildren.begin(), rchildren.end());
-        std::vector<Node> cargs;
-        cargs.push_back(op);
-        cargs.push_back(nullt);
-        // use n-ary rule, must reverse children
-        addAlfStep(AlfRule::NARY_CONG, res, rchildren, cargs, *cdp);
+        // use n-ary rule
+        addAlfStep(AlfRule::NARY_CONG, res, children, {op}, *cdp);
       }
       else
       {
@@ -223,20 +168,6 @@ bool AlfProofPostprocessCallback::update(Node res,
       }
     }
     break;
-    case ProofRule::CONCAT_CONFLICT:
-    {
-      if (children.size() == 1)
-      {
-        // no need to change
-        return false;
-      }
-      Assert(children.size() == 2);
-      Assert(children[0].getKind() == Kind::EQUAL);
-      Assert(children[0][0].getType().isSequence());
-      // must use the sequences version of the rule
-      addAlfStep(AlfRule::CONCAT_CONFLICT_DEQ, res, children, args, *cdp);
-    }
-    break;
     default: return false;
   }
   return true;
diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp
index b30f8986420..6b2372f12ac 100644
--- a/src/proof/alf/alf_printer.cpp
+++ b/src/proof/alf/alf_printer.cpp
@@ -48,6 +48,7 @@ bool AlfPrinter::isHandled(const ProofNode* pfn) const
   switch (pfn->getRule())
   {
     // List of handled rules
+    case ProofRule::SCOPE:
     case ProofRule::REFL:
     case ProofRule::SYMM:
     case ProofRule::TRANS:
@@ -128,6 +129,7 @@ bool AlfPrinter::isHandled(const ProofNode* pfn) const
     case ProofRule::REMOVE_TERM_FORMULA_AXIOM:
     case ProofRule::INSTANTIATE:
     case ProofRule::SKOLEMIZE:
+    case ProofRule::ALPHA_EQUIV:
     case ProofRule::ENCODE_PRED_TRANSFORM:
     case ProofRule::DSL_REWRITE:
     // alf rule is handled
@@ -405,18 +407,15 @@ void AlfPrinter::printStepPre(AlfPrintChannel* out, const ProofNode* pn)
 {
   // if we haven't yet allocated a proof id, do it now
   ProofRule r = pn->getRule();
-  if (r == ProofRule::ALF_RULE)
+  if (r == ProofRule::SCOPE)
   {
-    Assert(!pn->getArguments().empty());
-    Node rn = pn->getArguments()[0];
-    AlfRule ar = getAlfRule(rn);
-    if (ar == AlfRule::SCOPE)
+    const std::vector<Node>& args = pn->getArguments();
+    for (const Node& a : args)
     {
-      Assert(pn->getArguments().size() == 3);
-      size_t aid = allocateAssumePushId(pn);
-      Node a = d_tproc.convert(pn->getArguments()[2]);
+      size_t aid = allocateAssumePushId(pn, a);
+      Node aa = d_tproc.convert(a);
       // print a push
-      out->printAssume(a, aid, true);
+      out->printAssume(aa, aid, true);
     }
   }
 }
@@ -439,9 +438,6 @@ void AlfPrinter::getArgsFromProofRule(const ProofNode* pn,
       return;
     }
     break;
-    case ProofRule::ARITH_TRICHOTOMY:
-      // argument is redundant
-      return;
     case ProofRule::INSTANTIATE:
     {
       // ignore arguments past the term vector, collect them into an sexpr
@@ -475,7 +471,6 @@ void AlfPrinter::printStepPost(AlfPrintChannel* out, const ProofNode* pn)
   Assert(pn->getRule() != ProofRule::ASSUME);
   // if we have yet to allocate a proof id, do it now
   bool wasAlloc = false;
-  bool isPop = false;
   TNode conclusion = d_tproc.convert(pn->getResult());
   TNode conclusionPrint;
   // print conclusion only if option is set, or this is false
@@ -491,20 +486,10 @@ void AlfPrinter::printStepPost(AlfPrintChannel* out, const ProofNode* pn)
   {
     const std::vector<Node> aargs = pn->getArguments();
     Node rn = aargs[0];
-    AlfRule ar = getAlfRule(rn);
-    // if scope, do pop the assumption from passumeMap
-    if (ar == AlfRule::SCOPE)
-    {
-      isPop = true;
-      // note that aargs[1] is not provided, it is consumed as an assumption
-    }
-    else
+    // arguments are converted here
+    for (size_t i = 2, nargs = aargs.size(); i < nargs; i++)
     {
-      // arguments are converted here
-      for (size_t i = 2, nargs = aargs.size(); i < nargs; i++)
-      {
-        args.push_back(d_tproc.convert(aargs[i]));
-      }
+      args.push_back(d_tproc.convert(aargs[i]));
     }
   }
   else if (handled)
@@ -541,19 +526,54 @@ void AlfPrinter::printStepPost(AlfPrintChannel* out, const ProofNode* pn)
     premises.push_back(pid);
   }
   std::string rname = getRuleName(pn);
-  out->printStep(rname, conclusionPrint, id, premises, args, isPop);
+  if (r == ProofRule::SCOPE)
+  {
+    if (args.empty())
+    {
+      // If there are no premises, any reference to this proof can just refer to
+      // the body.
+      d_pletMap[pn] = premises[0];
+    }
+    else
+    {
+      // Assuming the body of the scope has identifier id_0, the following prints:
+      // (step-pop id_1 :rule scope :premises (id_0))
+      // ...
+      // (step-pop id_n :rule scope :premises (id_{n-1}))
+      // (step id :rule process_scope :premises (id_n) :args (C))
+      size_t tmpId;
+      for (size_t i = 0, nargs = args.size(); i < nargs; i++)
+      {
+        // Manually increment proof id counter and premises. Note they will only be
+        // used locally here to chain together the pops mentioned above.
+        tmpId = d_pfIdCounter;
+        d_pfIdCounter++;
+        out->printStep(rname, Node::null(), tmpId, premises, {}, true);
+        // The current id is the premises of the next.
+        premises.clear();
+        premises.push_back(tmpId);
+      }
+      // Finish with the process scope step.
+      std::vector<Node> pargs;
+      pargs.push_back(d_tproc.convert(children[0]->getResult()));
+      out->printStep("process_scope", conclusionPrint, id, premises, pargs);
+    }
+  }
+  else
+  {
+    out->printStep(rname, conclusionPrint, id, premises, args);
+  }
 }
 
-size_t AlfPrinter::allocateAssumePushId(const ProofNode* pn)
+size_t AlfPrinter::allocateAssumePushId(const ProofNode* pn, const Node& a)
 {
-  std::map<const ProofNode*, size_t>::iterator it = d_ppushMap.find(pn);
+  std::pair<const ProofNode*, Node> key(pn, a);
+  std::map<std::pair<const ProofNode*, Node>, size_t>::iterator it =
+      d_ppushMap.find(key);
   if (it != d_ppushMap.end())
   {
     return it->second;
   }
-  Assert(pn->getRule() == ProofRule::ALF_RULE);
-  // pn is a Alf SCOPE
-  Node a = pn->getArguments()[2];
   bool wasAlloc = false;
   size_t aid = allocateAssumeId(a, wasAlloc);
   // if we assigned an id to the assumption
@@ -563,7 +583,7 @@ size_t AlfPrinter::allocateAssumePushId(const ProofNode* pn)
     d_pfIdCounter++;
     aid = d_pfIdCounter;
   }
-  d_ppushMap[pn] = aid;
+  d_ppushMap[key] = aid;
   return aid;
 }
 
diff --git a/src/proof/alf/alf_printer.h b/src/proof/alf/alf_printer.h
index 886d50121cf..d56b0faf566 100644
--- a/src/proof/alf/alf_printer.h
+++ b/src/proof/alf/alf_printer.h
@@ -84,7 +84,7 @@ class AlfPrinter : protected EnvObj
    * return the identifier. pn should be an application of ProofNode::ALF_RULE
    * with AlfRule::SCOPE.
    */
-  size_t allocateAssumePushId(const ProofNode* pn);
+  size_t allocateAssumePushId(const ProofNode* pn, const Node& a);
   /**
    * Allocate (if necessary) the identifier for an assume step for the
    * assumption for formula n and return the identifier. Note this identifier is
@@ -103,7 +103,7 @@ class AlfPrinter : protected EnvObj
   /** Assume id counter */
   size_t d_pfIdCounter;
   /** Mapping scope proofs to identifiers */
-  std::map<const ProofNode*, size_t> d_ppushMap;
+  std::map<std::pair<const ProofNode*, Node>, size_t> d_ppushMap;
   /** Mapping proofs to identifiers */
   std::map<const ProofNode*, size_t> d_pletMap;
   /** Mapping assumed formulas to identifiers */
diff --git a/src/proof/alf/alf_proof_rule.cpp b/src/proof/alf/alf_proof_rule.cpp
index a9e45db2ff0..62f3407e000 100644
--- a/src/proof/alf/alf_proof_rule.cpp
+++ b/src/proof/alf/alf_proof_rule.cpp
@@ -28,9 +28,6 @@ const char* AlfRuleToString(AlfRule id)
   {
     case AlfRule::CONG: return "cong";
     case AlfRule::NARY_CONG: return "nary_cong";
-    case AlfRule::SCOPE: return "scope";
-    case AlfRule::PROCESS_SCOPE: return "process_scope";
-    case AlfRule::CONCAT_CONFLICT_DEQ: return "concat_conflict_deq";
     //================================================= Undefined rule
     case AlfRule::UNDEFINED: return "undefined";
     default: return "?";
diff --git a/src/proof/alf/alf_proof_rule.h b/src/proof/alf/alf_proof_rule.h
index 7a46751db63..c3022c52958 100644
--- a/src/proof/alf/alf_proof_rule.h
+++ b/src/proof/alf/alf_proof_rule.h
@@ -36,12 +36,6 @@ enum class AlfRule : uint32_t
   CONG,
   // n-ary congruence
   NARY_CONG,
-  // scope
-  SCOPE,
-  // process_scope
-  PROCESS_SCOPE,
-  // concat conflict disequality
-  CONCAT_CONFLICT_DEQ,
   // Used in case that a step in the proof rule could not be translated.
   UNDEFINED
 };
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 302b2f7299a..43532525503 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -231,7 +231,8 @@ std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(
 
 void PfManager::printProof(std::ostream& out,
                            std::shared_ptr<ProofNode> fp,
-                           options::ProofFormatMode mode)
+                           options::ProofFormatMode mode,
+                           const std::map<Node, std::string>& assertionNames)
 {
   Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
   // We don't want to invalidate the proof nodes in fp, since these may be
@@ -272,7 +273,7 @@ void PfManager::printProof(std::ostream& out,
         d_env, anc, options().proof.proofAletheResPivots);
     vpfpp.process(fp);
     proof::AletheProofPrinter vpp(d_env);
-    vpp.print(out, fp);
+    vpp.print(out, fp, assertionNames);
   }
   else if (mode == options::ProofFormatMode::LFSC)
   {
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index f678aee6632..94a58d76864 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -95,7 +95,9 @@ class PfManager : protected EnvObj
    */
   void printProof(std::ostream& out,
                   std::shared_ptr<ProofNode> fp,
-                  options::ProofFormatMode mode);
+                  options::ProofFormatMode mode,
+                  const std::map<Node, std::string>& assertionNames =
+                      std::map<Node, std::string>());
 
   /**
    * Translate difficulty map. This takes a mapping dmap from preprocessed
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 12d0b9e37e8..941af90f2bc 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1396,7 +1396,8 @@ std::vector<Node> SolverEngine::convertPreprocessedToInput(
 
 void SolverEngine::printProof(std::ostream& out,
                               std::shared_ptr<ProofNode> fp,
-                              modes::ProofFormat proofFormat)
+                              modes::ProofFormat proofFormat,
+                              const std::map<Node, std::string>& assertionNames)
 {
   // we print in the format based on the proof mode
   options::ProofFormatMode mode = options::ProofFormatMode::NONE;
@@ -1413,7 +1414,7 @@ void SolverEngine::printProof(std::ostream& out,
     case modes::ProofFormat::LFSC: mode = options::ProofFormatMode::LFSC; break;
   }
 
-  d_pfManager->printProof(out, fp, mode);
+  d_pfManager->printProof(out, fp, mode, assertionNames);
   out << std::endl;
 }
 
diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 5b98abc9208..a3b77df4d56 100644
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -1047,7 +1047,8 @@ class CVC5_EXPORT SolverEngine
    */
   void printProof(std::ostream& out,
                   std::shared_ptr<ProofNode> fp,
-                  modes::ProofFormat proofFormat);
+                  modes::ProofFormat proofFormat,
+                  const std::map<Node, std::string>& assertionNames);
 
   /* Members -------------------------------------------------------------- */
 
diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp
index 09f2821abd8..c50a08c24d7 100644
--- a/src/theory/arith/branch_and_bound.cpp
+++ b/src/theory/arith/branch_and_bound.cpp
@@ -105,7 +105,8 @@ std::vector<TrustNode> BranchAndBound::branchIntegerVariable(TNode var,
           pnm->mkNode(ProofRule::CONTRA,
                       {pnm->mkNode(ProofRule::ARITH_TRICHOTOMY,
                                    {pnm->mkAssume(less.negate()), pfNotRawEq},
-                                   {greater}),
+                                   {},
+                                   greater),
                        pnm->mkAssume(greater.negate())},
                       {});
       std::vector<Node> assumptions = {
diff --git a/src/theory/arith/linear/approx_simplex.cpp b/src/theory/arith/linear/approx_simplex.cpp
index 15fb3ae96ed..336fa52db38 100644
--- a/src/theory/arith/linear/approx_simplex.cpp
+++ b/src/theory/arith/linear/approx_simplex.cpp
@@ -136,8 +136,8 @@ struct CutScratchPad {
   }
 };
 
-class GmiInfo;
-class MirInfo;
+struct GmiInfo;
+struct MirInfo;
 class BranchCutInfo;
 
 class ApproxGLPK : public ApproximateSimplex
@@ -257,10 +257,6 @@ class ApproxGLPK : public ApproximateSimplex
   bool replaceSlacksOnCuts();
   bool loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound& tmp);
 
-  double sumInfeasibilities(bool mip) const
-  {
-    return sumInfeasibilities(mip? d_mipProb : d_realProb);
-  }
   double sumInfeasibilities(glp_prob* prob, bool mip) const;
 
   /** UTILITIES FOR DEALING WITH ESTIMATES */
diff --git a/src/theory/arith/linear/congruence_manager.cpp b/src/theory/arith/linear/congruence_manager.cpp
index 5d584b3fe58..2f6ae20124e 100644
--- a/src/theory/arith/linear/congruence_manager.cpp
+++ b/src/theory/arith/linear/congruence_manager.cpp
@@ -188,8 +188,8 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP
   if (isProofEnabled())
   {
     pf = d_pnm->mkNode(
-        ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eqC->getProofLiteral()});
-    pf = d_pnm->mkNode(ProofRule::MACRO_SR_PRED_TRANSFORM, {pf}, {eq});
+        ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {}, eqC->getProofLiteral());
+    pf = d_pnm->mkNode(ProofRule::MACRO_SR_PRED_TRANSFORM, {pf}, {eq}, eq);
   }
 
   d_keepAlive.push_back(reason);
@@ -601,7 +601,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
   std::shared_ptr<ProofNode> pf;
   if (isProofEnabled())
   {
-    pf = d_pnm->mkNode(ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eq});
+    pf = d_pnm->mkNode(ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {}, eq);
   }
   d_keepAlive.push_back(eq);
   d_keepAlive.push_back(reason);
diff --git a/src/theory/arith/linear/constraint.cpp b/src/theory/arith/linear/constraint.cpp
index edba04ada72..e50c158b965 100644
--- a/src/theory/arith/linear/constraint.cpp
+++ b/src/theory/arith/linear/constraint.cpp
@@ -1849,10 +1849,8 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
         }
         case ArithProofType::TrichotomyAP:
         {
-          pf = pnm->mkNode(ProofRule::ARITH_TRICHOTOMY,
-                           children,
-                           {getProofLiteral()},
-                           getProofLiteral());
+          pf = pnm->mkNode(
+              ProofRule::ARITH_TRICHOTOMY, children, {}, getProofLiteral());
           break;
         }
         case ArithProofType::InternalAssumeAP:
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 37660c05096..8cbdca9eb9d 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -399,10 +399,8 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
                                  {exp[1][0]},
                                  {rb});
                 }
-                proof->addStep(simpleeq,
-                               ProofRule::ARITH_TRICHOTOMY,
-                               {lb, rb},
-                               {simpleeq});
+                proof->addStep(
+                    simpleeq, ProofRule::ARITH_TRICHOTOMY, {lb, rb}, {});
                 proof->addStep(
                     tmplem[0], ProofRule::AND_INTRO, {exp[0], simpleeq}, {});
                 proof->addStep(tmplem[1],
diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp
index a0d5205620a..7919de76202 100644
--- a/src/theory/arith/proof_checker.cpp
+++ b/src/theory/arith/proof_checker.cpp
@@ -310,29 +310,37 @@ Node ArithProofRuleChecker::checkInternal(ProofRule id,
     {
       Node a = negateProofLiteral(children[0]);
       Node b = negateProofLiteral(children[1]);
-      Node c = args[0];
-      if (a[0] == b[0] && b[0] == c[0] && a[1] == b[1] && b[1] == c[1])
+      if (a[0] == b[0] && a[1] == b[1])
       {
         std::set<Kind> cmps;
         cmps.insert(a.getKind());
         cmps.insert(b.getKind());
-        cmps.insert(c.getKind());
+        Kind retk = Kind::UNDEFINED_KIND;
         if (cmps.count(Kind::EQUAL) == 0)
         {
-          Trace("arith::pf::check") << "Error: No = " << std::endl;
-          return Node::null();
+          retk = Kind::EQUAL;
         }
         if (cmps.count(Kind::GT) == 0)
         {
-          Trace("arith::pf::check") << "Error: No > " << std::endl;
-          return Node::null();
+          if (retk != Kind::UNDEFINED_KIND)
+          {
+            Trace("arith::pf::check")
+                << "Error: No GT and " << retk << std::endl;
+            return Node::null();
+          }
+          retk = Kind::GT;
         }
         if (cmps.count(Kind::LT) == 0)
         {
-          Trace("arith::pf::check") << "Error: No < " << std::endl;
-          return Node::null();
+          if (retk != Kind::UNDEFINED_KIND)
+          {
+            Trace("arith::pf::check")
+                << "Error: No LT and " << retk << std::endl;
+            return Node::null();
+          }
+          retk = Kind::LT;
         }
-        return args[0];
+        return nm->mkNode(retk, a[0], a[1]);
       }
       else
       {
@@ -340,7 +348,6 @@ Node ArithProofRuleChecker::checkInternal(ProofRule id,
             << "Error: Different polynomials / values" << std::endl;
         Trace("arith::pf::check") << "  a: " << a << std::endl;
         Trace("arith::pf::check") << "  b: " << b << std::endl;
-        Trace("arith::pf::check") << "  c: " << c << std::endl;
         return Node::null();
       }
       // Check that all have the same constant:
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 3b530f4bb4a..1b3e7af0923 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -209,12 +209,9 @@ TrustNode AlphaEquivalence::reduceQuantifier(Node q)
   {
     std::vector<Node> pfArgs;
     pfArgs.push_back(ret);
-    for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
-    {
-      pfArgs.push_back(vars[i].eqNode(subs[i]));
-      Trace("alpha-eq") << "subs: " << vars[i] << " -> " << subs[i]
-                        << std::endl;
-    }
+    NodeManager* nm = NodeManager::currentNM();
+    pfArgs.push_back(nm->mkNode(Kind::SEXPR, vars));
+    pfArgs.push_back(nm->mkNode(Kind::SEXPR, subs));
     CDProof cdp(d_env);
     Node sret =
         ret.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp
index 1e995535be2..b58e6575f14 100644
--- a/src/theory/quantifiers/proof_checker.cpp
+++ b/src/theory/quantifiers/proof_checker.cpp
@@ -101,29 +101,31 @@ Node QuantifiersProofRuleChecker::checkInternal(
   else if (id == ProofRule::ALPHA_EQUIV)
   {
     Assert(children.empty());
-    // arguments must be equalities that are bound variables that are
-    // pairwise unique
+    Assert(args.size() == 3);
+    // must be lists of the same length
+    if (args[1].getKind() != Kind::SEXPR || args[2].getKind() != Kind::SEXPR
+        || args[1].getNumChildren() != args[2].getNumChildren())
+    {
+      return Node::null();
+    }
+    // arguments must be lists of bound variables that are pairwise unique
     std::unordered_set<Node> allVars[2];
     std::vector<Node> vars;
     std::vector<Node> newVars;
-    for (size_t i = 1, nargs = args.size(); i < nargs; i++)
+    for (size_t i = 0, nargs = args[1].getNumChildren(); i < nargs; i++)
     {
-      if (args[i].getKind() != Kind::EQUAL)
-      {
-        return Node::null();
-      }
-      for (size_t j = 0; j < 2; j++)
+      for (size_t j = 1; j <= 2; j++)
       {
-        Node v = args[i][j];
-        if (v.getKind() != Kind::BOUND_VARIABLE
-            || allVars[j].find(v) != allVars[j].end())
+        Node v = args[j][i];
+        std::unordered_set<Node>& av = allVars[j - 1];
+        if (v.getKind() != Kind::BOUND_VARIABLE || av.find(v) != av.end())
         {
           return Node::null();
         }
-        allVars[j].insert(v);
+        av.insert(v);
       }
-      vars.push_back(args[i][0]);
-      newVars.push_back(args[i][1]);
+      vars.push_back(args[1][i]);
+      newVars.push_back(args[2][i]);
     }
     Node renamedBody = args[0].substitute(
         vars.begin(), vars.end(), newVars.begin(), newVars.end());
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index f97d9cec8db..5df8f466c32 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -196,8 +196,29 @@ void QuantifiersRewriter::computeArgVec2(const std::vector<Node>& args,
   }
 }
 
-RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
-  return RewriteResponse(REWRITE_DONE, in);
+RewriteResponse QuantifiersRewriter::preRewrite(TNode q)
+{
+  Kind k = q.getKind();
+  if (k == Kind::FORALL || k == Kind::EXISTS)
+  {
+    // Do prenex merging now, since this may impact trigger selection.
+    // In particular consider:
+    //   (forall ((x Int)) (forall ((y Int)) (! (P x) :pattern ((f x)))))
+    // If we wait until post-rewrite, we would rewrite the inner quantified
+    // formula, dropping the pattern, so the entire formula becomes:
+    //   (forall ((x Int)) (P x))
+    // Instead, we merge to:
+    //   (forall ((x Int) (y Int)) (! (P x) :pattern ((f x))))
+    // eagerly here, where after we would drop y to obtain:
+    //   (forall ((x Int)) (! (P x) :pattern ((f x))))
+    // See issue #10303.
+    Node qm = mergePrenex(q);
+    if (q != qm)
+    {
+      return RewriteResponse(REWRITE_AGAIN_FULL, qm);
+    }
+  }
+  return RewriteResponse(REWRITE_DONE, q);
 }
 
 RewriteResponse QuantifiersRewriter::postRewrite(TNode in)
@@ -222,50 +243,10 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in)
   }
   else if (in.getKind() == Kind::FORALL)
   {
-    std::vector<Node> boundVars;
-    Node body = in;
-    bool combineQuantifiers = false;
-    bool continueCombine = false;
-    do
-    {
-      for (const Node& v : body[0])
-      {
-        if (std::find(boundVars.begin(), boundVars.end(), v)==boundVars.end())
-        {
-          boundVars.push_back(v);
-        }
-      }
-      continueCombine = false;
-      if (body.getNumChildren() == 2 && body[1].getKind() == Kind::FORALL)
-      {
-        QAttributes qa;
-        QuantAttributes::computeQuantAttributes(body[1], qa);
-        // should never combine a quantified formula with a pool or
-        // non-standard quantified formula here.
-        // note that we technically should check
-        // doOperation(body[1], COMPUTE_PRENEX, qa) here, although this
-        // is too restrictive, as sometimes nested patterns should just be
-        // applied to the top level.
-        if (qa.isStandard() && !qa.d_hasPool)
-        {
-          body = body[1];
-          continueCombine = true;
-          combineQuantifiers = true;
-        }
-      }
-    }
-    while (continueCombine);
-    if (combineQuantifiers)
+    // do prenex merging
+    ret = mergePrenex(in);
+    if (ret != in)
     {
-      NodeManager* nm = NodeManager::currentNM();
-      std::vector<Node> children;
-      children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, boundVars));
-      children.push_back(body[1]);
-      if (body.getNumChildren() == 3)
-      {
-        children.push_back(body[2]);
-      }
-      ret = nm->mkNode(Kind::FORALL, children);
       status = REWRITE_AGAIN_FULL;
     }
     else if (in[1].isConst() && in.getNumChildren() == 2)
@@ -300,6 +281,59 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in)
   return RewriteResponse( status, ret );
 }
 
+Node QuantifiersRewriter::mergePrenex(const Node& q)
+{
+  Assert(q.getKind() == Kind::FORALL || q.getKind() == Kind::EXISTS);
+  Kind k = q.getKind();
+  std::vector<Node> boundVars;
+  Node body = q;
+  bool combineQuantifiers = false;
+  bool continueCombine = false;
+  do
+  {
+    for (const Node& v : body[0])
+    {
+      if (std::find(boundVars.begin(), boundVars.end(), v) == boundVars.end())
+      {
+        boundVars.push_back(v);
+      }
+    }
+    continueCombine = false;
+    if (body.getNumChildren() == 2 && body[1].getKind() == k)
+    {
+      QAttributes qa;
+      QuantAttributes::computeQuantAttributes(body[1], qa);
+      // Should never combine a quantified formula with a pool or
+      // non-standard quantified formula here.
+      // Note that we technically should check
+      // doOperation(body[1], COMPUTE_PRENEX, qa) here, although this
+      // is too restrictive, as sometimes nested patterns should just be
+      // applied to the top level, for example:
+      // (forall ((x Int)) (forall ((y Int)) (! P :pattern ((f x y)))))
+      // should be a pattern for the top-level quantifier here.
+      if (qa.isStandard() && !qa.d_hasPool)
+      {
+        body = body[1];
+        continueCombine = true;
+        combineQuantifiers = true;
+      }
+    }
+  } while (continueCombine);
+  if (combineQuantifiers)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    std::vector<Node> children;
+    children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, boundVars));
+    children.push_back(body[1]);
+    if (body.getNumChildren() == 3)
+    {
+      children.push_back(body[2]);
+    }
+    return nm->mkNode(k, children);
+  }
+  return q;
+}
+
 bool QuantifiersRewriter::addCheckElimChild(std::vector<Node>& children,
                                             Node c,
                                             Kind k,
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 3553f2cdc07..36f61219e33 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -217,6 +217,13 @@ class QuantifiersRewriter : public TheoryRewriter
   static bool isStandard(QAttributes& qa, const Options& opts);
 
  private:
+  /**
+   * Do trivial merging of the prenex of quantified formula q, e.g.
+   * (forall ((x Int)) (forall ((y Int)) (P x y))) --->
+   * (forall ((x Int) (y Int)) (P x y)).
+   * This is done until fixed point.
+   */
+  Node mergePrenex(const Node& q);
   /**
    * Helper method for getVarElim, called when n has polarity pol in body.
    */
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 2d196fda030..00ac11f501d 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -434,6 +434,7 @@ void InferProofCons::convert(InferenceId infer,
         std::vector<Node> childrenC;
         childrenC.push_back(mainEqCeq);
         // if it is between sequences, we require the explicit disequality
+        ProofRule r = ProofRule::CONCAT_CONFLICT;
         if (mainEqCeq[0].getType().isSequence())
         {
           Assert(t0.isConst() && s0.isConst());
@@ -442,11 +443,11 @@ void InferProofCons::convert(InferenceId infer,
           psb.addStep(ProofRule::MACRO_SR_PRED_INTRO, {}, {deq}, deq);
           Assert(!deq.isNull());
           childrenC.push_back(deq);
+          r = ProofRule::CONCAT_CONFLICT_DEQ;
         }
         std::vector<Node> argsC;
         argsC.push_back(nodeIsRev);
-        Node conflict =
-            psb.tryStep(ProofRule::CONCAT_CONFLICT, childrenC, argsC);
+        Node conflict = psb.tryStep(r, childrenC, argsC);
         if (conflict == conc)
         {
           useBuffer = true;
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index ccdf5b40ca8..c620170cc62 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -37,6 +37,7 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(ProofRule::CONCAT_EQ, this);
   pc->registerChecker(ProofRule::CONCAT_UNIFY, this);
   pc->registerChecker(ProofRule::CONCAT_CONFLICT, this);
+  pc->registerChecker(ProofRule::CONCAT_CONFLICT_DEQ, this);
   pc->registerChecker(ProofRule::CONCAT_SPLIT, this);
   pc->registerChecker(ProofRule::CONCAT_CSPLIT, this);
   pc->registerChecker(ProofRule::CONCAT_LPROP, this);
@@ -179,7 +180,8 @@ Node StringProofRuleChecker::checkInternal(ProofRule id,
       }
       return children[1][0][0].eqNode(children[1][1][0]);
     }
-    else if (id == ProofRule::CONCAT_CONFLICT)
+    else if (id == ProofRule::CONCAT_CONFLICT
+             || id == ProofRule::CONCAT_CONFLICT_DEQ)
     {
       Assert(children.size() >= 1 && children.size() <= 2);
       if (!t0.isConst() || !s0.isConst())
@@ -196,9 +198,9 @@ Node StringProofRuleChecker::checkInternal(ProofRule id,
         return Node::null();
       }
       // if a disequality was provided, ensure that it is correct
-      if (children.size() == 2)
+      if (id == ProofRule::CONCAT_CONFLICT_DEQ)
       {
-        if (children[1].getKind() != Kind::NOT
+        if (children.size() != 2 || children[1].getKind() != Kind::NOT
             || children[1][0].getKind() != Kind::EQUAL
             || children[1][0][0] != t0 || children[1][0][1] != s0)
         {
@@ -207,7 +209,7 @@ Node StringProofRuleChecker::checkInternal(ProofRule id,
       }
       else if (t0.getType().isSequence())
       {
-        // we require the disequality for sequences
+        // we require the CONCAT_CONFLICT_DEQ for sequences
         return Node::null();
       }
       return nm->mkConst(false);
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 396f3890f02..3dd560dbaef 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2628,6 +2628,7 @@ set(regress_1_tests
   regress1/quantifiers/choice-move-delta-relt.smt2
   regress1/quantifiers/const.cvc.smt2
   regress1/quantifiers/constfunc.cvc.smt2
+  regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 
   regress1/quantifiers/dd.bug812-ieval.smt2
   regress1/quantifiers/ddatv-delta2.smt2
   regress1/quantifiers/dt-tc-opt-small.smt2
diff --git a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2
new file mode 100644
index 00000000000..2253b8cde8c
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: -q
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort e 0)
+(declare-sort p 0)
+(declare-fun t (p) Int)
+(declare-fun o (Int) p)
+(assert (forall ((x Int)) (! (= 0 x) :pattern ((o x)))))
+(declare-datatypes ((s 0)) (((s_1 (x e) (e2 e) (c e) (c_ p)))))
+(declare-datatypes ((us 0)) (((re (_s s)))))
+(declare-datatypes ((_s2 0)) (((s_ (e3 (Array Int us))))))
+(declare-datatypes ((us_ 0)) (((us4 (us3 _s2)))))
+(declare-datatypes ((s_2 0)) (((us2 (re2 Bool)))))
+(declare-datatypes ((u 0)) (((us5 (_s3 s_2)))))
+(declare-fun e1 (us_ Int) (Array Int u))
+(declare-const r e)
+(assert (forall ((p1 us_)) (forall ((a Int)) (! (not (ite (forall ((i Int)) (= (t (c_ (_s (select (e3 (us3 p1)) i)))) (t (c_ (_s (re (s_1 r r r (o 0)))))))) true false)) :pattern ((e1 p1 0))))))
+(assert (exists ((f _s2)) (or (forall ((n Int)) (or (forall ((j Int)) (= true (re2 (_s3 (select (e1 (us4 f) 0) 0))))))))))
+(check-sat)