diff --git a/Smt/Preprocess/Iff.lean b/Smt/Preprocess/Iff.lean
index 19e1c79e..5c868dac 100644
--- a/Smt/Preprocess/Iff.lean
+++ b/Smt/Preprocess/Iff.lean
@@ -28,7 +28,7 @@ def elimIff (mv : MVarId) (hs : List Expr) : MetaM (List Expr × MVarId) := mv.w
   let simpTheorems ← #[``eq_self, ``iff_eq_eq].foldlM (·.addConst ·) ({} : Meta.SimpTheorems)
   let simpTheorems := #[simpTheorems]
   let congrTheorems ← Meta.getSimpCongrTheorems
-  let ctx := { simpTheorems, congrTheorems }
+  let ctx ← Meta.Simp.mkContext {} simpTheorems congrTheorems
   let (hs, mv) ← elimIffLocalDecls mv hs ctx
   let mv ← elimIffTarget mv ctx
   return (hs, mv)
diff --git a/Smt/Reconstruct/BitVec.lean b/Smt/Reconstruct/BitVec.lean
index 4c4f791c..f9a4ac95 100644
--- a/Smt/Reconstruct/BitVec.lean
+++ b/Smt/Reconstruct/BitVec.lean
@@ -262,7 +262,8 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
       let ps := [``Nat.reduceAdd, ``Nat.reduceLT, ``reduceDIte]
       let simpTheorems ← ds.foldrM (fun n a => a.addDeclToUnfold n) {}
       let simpProcs ← ps.foldrM (fun n a => a.add n false) {}
-      let (some mv, _) ← Meta.simpTarget mv { simpTheorems := #[simpTheorems] } simpProcs | throwError "simp failed"
+      let ctx ← Meta.Simp.mkContext {} #[simpTheorems]
+      let (some mv, _) ← Meta.simpTarget mv ctx simpProcs | throwError "simp failed"
       mv.refl
       addThm q($x = $x') q(Eq.trans (BitVec.self_eq_bb $x) $h)
     | .EQUAL =>
@@ -278,8 +279,9 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
       let ps := [``Nat.reduceAdd, ``Nat.reduceSub, ``Nat.reduceEqDiff, ``reduceIte]
       let simpTheorems ← ds.foldrM (fun n a => a.addDeclToUnfold n) {}
       let simpTheorems ← ts.foldrM (fun n a => a.addConst n) simpTheorems
+      let ctx ← Meta.Simp.mkContext {} #[simpTheorems]
       let simpProcs ← ps.foldrM (fun n a => a.add n false) {}
-      let (some mv, _) ← Meta.simpTarget mv { simpTheorems := #[simpTheorems] } simpProcs | throwError "simp failed"
+      let (some mv, _) ← Meta.simpTarget mv ctx simpProcs | throwError "simp failed"
       mv.refl
       addThm q(($x = $y) = $p) q(Eq.trans (BitVec.eq_eq_beq $x $y) (Bool.eq_of_decide_eq $h))
     | .BITVECTOR_ADD =>
@@ -294,8 +296,9 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
       let ps := [``Nat.reduceAdd, ``Nat.reduceLT, ``reduceDIte, ``reduceIte]
       let simpTheorems ← ds.foldrM (fun n a => a.addDeclToUnfold n) {}
       let simpTheorems ← ts.foldrM (fun n a => a.addConst n) simpTheorems
+      let ctx ← Meta.Simp.mkContext {} #[simpTheorems]
       let simpProcs ← ps.foldrM (fun n a => a.add n false) {}
-      let (some mv, _) ← Meta.simpTarget mv { simpTheorems := #[simpTheorems] } simpProcs | throwError "simp failed"
+      let (some mv, _) ← Meta.simpTarget mv ctx simpProcs | throwError "simp failed"
       mv.refl
       addThm q($x + $y = $z) q(Eq.trans (BitVec.add_eq_adc' $x $y) $h)
     | _ => return none
diff --git a/Smt/Reconstruct/Bool/Tactic.lean b/Smt/Reconstruct/Bool/Tactic.lean
index 511ae32b..8c12cc00 100644
--- a/Smt/Reconstruct/Bool/Tactic.lean
+++ b/Smt/Reconstruct/Bool/Tactic.lean
@@ -21,7 +21,8 @@ def traceBoolify (r : Except Exception MVarId) : MetaM MessageData :=
 def boolify (mv : MVarId) : MetaM MVarId := withTraceNode `smt.reconstruct.boolify traceBoolify do
   let ns := [``Bool.decide_eq_true, ``decide_true_eq, ``decide_false_eq, ``decide_not_eq, ``decide_and_eq, ``decide_or_eq, ``decide_eq_eq, ``decide_xor_eq]
   let simpTheorems ← ns.foldrM (fun n a => a.addTheorem (.decl n) (.const n [])) {}
-  let (some mv, _) ← Meta.simpTarget mv { simpTheorems } | throwError "failed to boolify goal:{mv}"
+  let ctx ← Meta.Simp.mkContext {} simpTheorems
+  let (some mv, _) ← Meta.simpTarget mv ctx | throwError "failed to boolify goal:{mv}"
   return mv
 
 namespace Tactic
diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean
index 2a6040d6..2052c0ea 100644
--- a/Smt/Reconstruct/Rat.lean
+++ b/Smt/Reconstruct/Rat.lean
@@ -15,8 +15,7 @@ import Smt.Reconstruct.Rewrite
 
 namespace Smt.Reconstruct.Rat
 
-open Lean hiding Rat
-open Qq
+open Lean Qq
 
 @[smt_sort_reconstruct] def reconstructRatSort : SortReconstructor := fun s => do match s.getKind with
   | .REAL_SORT => return q(Rat)
@@ -27,7 +26,7 @@ open Qq
     | .DIV_BY_ZERO => return q(fun (x : Rat) => x / 0)
     | _ => return none
   | .CONST_RATIONAL =>
-    let c : Lean.Rat := t.getRationalValue!
+    let c : Std.Internal.Rat := t.getRationalValue!
     let num : Q(Rat) := mkRatLit c.num.natAbs
     if c.den == 1 then
       if c.num ≥ 0 then
@@ -311,7 +310,7 @@ where
       return ha
 
 def reconstructArithPolyNormRel (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
-  let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
+  let lcx : Std.Internal.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
   let cx : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
   let cy : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]![0]!
   let x₁ : Q(Rat) ← reconstructTerm pf.getResult[0]![0]!
diff --git a/Smt/Reconstruct/Rat/Polynorm.lean b/Smt/Reconstruct/Rat/Polynorm.lean
index 05004b70..c97f70ec 100644
--- a/Smt/Reconstruct/Rat/Polynorm.lean
+++ b/Smt/Reconstruct/Rat/Polynorm.lean
@@ -283,8 +283,7 @@ theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : RatExpr} (h : e₁.toPolynom
 
 end PolyNorm.RatExpr
 
-open Lean hiding Rat
-open Qq
+open Lean Qq
 
 abbrev PolyM := StateT (Array Q(Int) × Array Q(Rat)) MetaM
 
diff --git a/Smt/Reconstruct/Real.lean b/Smt/Reconstruct/Real.lean
index 53b1f791..48ca01f4 100644
--- a/Smt/Reconstruct/Real.lean
+++ b/Smt/Reconstruct/Real.lean
@@ -25,7 +25,7 @@ open Lean Qq
     | .DIV_BY_ZERO => return q(fun (x : Real) => x / 0)
     | _ => return none
   | .CONST_RATIONAL =>
-    let c : Lean.Rat := t.getRationalValue!
+    let c : Std.Internal.Rat := t.getRationalValue!
     let num : Q(Real) := mkRealLit c.num.natAbs
     if c.den == 1 then
       if c.num ≥ 0 then
@@ -318,7 +318,7 @@ where
       return ha
 
 def reconstructArithPolyNormRel (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
-  let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
+  let lcx : Std.Internal.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
   let cx : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
   let cy : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[1]![0]!
   let x₁ : Q(Real) ← reconstructTerm pf.getResult[0]![0]!
diff --git a/Smt/Reconstruct/Real/Polynorm.lean b/Smt/Reconstruct/Real/Polynorm.lean
index 4dba60fc..6842265f 100644
--- a/Smt/Reconstruct/Real/Polynorm.lean
+++ b/Smt/Reconstruct/Real/Polynorm.lean
@@ -290,8 +290,7 @@ theorem denote_eq_from_toPolynomial_eq {e₁ e₂ : RealExpr} (h : e₁.toPolyno
 
 end PolyNorm.RealExpr
 
-open Lean hiding Rat
-open Qq
+open Lean Qq
 
 abbrev PolyM := StateT (Array Q(Int) × Array Q(Real)) MetaM
 
@@ -397,7 +396,7 @@ def traceArithNormNum (r : Except Exception Unit) : MetaM MessageData :=
 
 open Mathlib.Meta.NormNum in
 def normNum (mv : MVarId) : MetaM Unit := withTraceNode `smt.reconstruct.normNum traceArithNormNum do
-  if let some (_, mv) ← normNumAt mv {} #[] true false then
+  if let some (_, mv) ← normNumAt mv (← Meta.Simp.mkContext) #[] true false then
     throwError "[norm_num]: could not prove {← mv.getType}"
 
 namespace Tactic
diff --git a/Smt/Tactic/EqnDef.lean b/Smt/Tactic/EqnDef.lean
index c4c843f7..f86d255b 100644
--- a/Smt/Tactic/EqnDef.lean
+++ b/Smt/Tactic/EqnDef.lean
@@ -172,7 +172,7 @@ def specializeEqnDef (x : FVarId) (args : Array Expr) (opaqueConsts : Std.HashSe
         let (fvEq, mvarId) ← (← mvarId.assert (nm ++ `specialization) eqnRw pfRw).intro1P
         return (fvEq, [mvarId])
 
-syntax blockingConsts := "blocking [" term,* "]"
+syntax blockingConsts := "blocking" "[" term,* "]"
 
 /-- `specialize_def foo [arg₁, ⋯, argₙ]` introduces a new equational definition `foo.arg₁.⋯.argₙ`
 whose body is the partial evaluation of `foo arg₁ ⋯ argₙ`. During reduction, all SMT-LIB builtins
diff --git a/Smt/Tactic/Smt.lean b/Smt/Tactic/Smt.lean
index a5d4865d..81f096ef 100644
--- a/Smt/Tactic/Smt.lean
+++ b/Smt/Tactic/Smt.lean
@@ -82,7 +82,7 @@ def smt (mv : MVarId) (hs : List Expr) (timeout : Option Nat := none) : MetaM (L
 namespace Tactic
 
 syntax smtHints := ("[" term,* "]")?
-syntax smtTimeout := ("(timeout := " num ")")?
+syntax smtTimeout := ("(" "timeout" " := " num ")")?
 
 /-- `smt` converts the current goal into an SMT query and checks if it is
 satisfiable. By default, `smt` generates the minimum valid SMT query needed to
diff --git a/Smt/Tactic/WHNFConfigurable.lean b/Smt/Tactic/WHNFConfigurable.lean
index 97b8abf8..20008626 100644
--- a/Smt/Tactic/WHNFConfigurable.lean
+++ b/Smt/Tactic/WHNFConfigurable.lean
@@ -223,7 +223,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
         trace[Smt.reduce.rec] "failed."
         failK ()
 
-    let major ← whnf <| recArgs.get ⟨majorIdx, h⟩
+    let major ← whnf <| recArgs[majorIdx]'h
     if (← read).letPushElim then
       letTelescopeAbstracting major fun _ major abs => do
         let e' ← cont major
@@ -244,7 +244,7 @@ private def reduceQuotRec (recVal  : QuotVal) (recArgs : Array Expr)
     : ReductionM α :=
   let process (majorPos argPos : Nat) : ReductionM α :=
     if h : majorPos < recArgs.size then do
-      let major := recArgs.get ⟨majorPos, h⟩
+      let major := recArgs[majorPos]'h
       let major ← whnf major
       match major with
       | Expr.app (Expr.app (Expr.app (Expr.const majorFn _) _) _) majorArg => do
@@ -273,7 +273,7 @@ mutual
     else do
       let majorIdx := recVal.getMajorIdx
       if h : majorIdx < recArgs.size then do
-        let major := recArgs.get ⟨majorIdx, h⟩
+        let major := recArgs[majorIdx]'h
         let major ← whnf major
         getStuckMVar? major
       else
@@ -282,7 +282,7 @@ mutual
   private partial def isQuotRecStuck? (recVal : QuotVal) (recArgs : Array Expr) : ReductionM (Option MVarId) :=
     let process? (majorPos : Nat) : ReductionM (Option MVarId) :=
       if h : majorPos < recArgs.size then do
-        let major := recArgs.get ⟨majorPos, h⟩
+        let major := recArgs[majorPos]'h
         let major ← whnf major
         getStuckMVar? major
       else
@@ -440,9 +440,9 @@ private def whnfMatcher (e : Expr) : ReductionM Expr := do
   let mut transparency ← getTransparency
   if transparency == TransparencyMode.reducible then
     transparency := TransparencyMode.instances
-  withTransparency transparency <|
-    withTheReader Meta.Context (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher ctx.canUnfold? }) do
-      whnf e
+  withTransparency transparency do
+    let ctx ← readThe Meta.Context
+    withCanUnfoldPred (canUnfoldAtMatcher ctx.canUnfold?) (whnf e)
 
 def reduceMatcher? (e : Expr) : ReductionM ReduceMatcherResult := do
   trace[Smt.reduce.matcher] "{e}"
@@ -702,7 +702,7 @@ where
 
 def shouldUnfold (ci : ConstantInfo) : ReductionM Bool := do
   let some canUnfold := (← readThe Meta.Context).canUnfold? | return true
-  let cfg := (← readThe Meta.Context).config
+  let cfg ← getConfig (← readThe Meta.Context)
   canUnfold cfg ci
 
 mutual
@@ -930,17 +930,18 @@ def reduceNat? (e : Expr) : ReductionM (Option Expr) :=
 @[inline] private def cached? (useCache : Bool) (e : Expr) : MetaM (Option Expr) := do
   if useCache then
     match (← getConfig).transparency with
-    | TransparencyMode.default => return (← get).cache.whnfDefault.find? e
-    | TransparencyMode.all     => return (← get).cache.whnfAll.find? e
+    | TransparencyMode.default => return (← get).cache.whnf.find? (← mkExprConfigCacheKey e)
+    | TransparencyMode.all     => return (← get).cache.whnf.find? (← mkExprConfigCacheKey e)
     | _                        => unreachable!
   else
     return none
 
 private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
   if useCache then
+    let ecck ← mkExprConfigCacheKey e
     match (← getConfig).transparency with
-    | TransparencyMode.default => modify fun s => { s with cache.whnfDefault := s.cache.whnfDefault.insert e r }
-    | TransparencyMode.all     => modify fun s => { s with cache.whnfAll     := s.cache.whnfAll.insert e r }
+    | TransparencyMode.default => modify fun s => { s with cache.whnf := s.cache.whnf.insert ecck r }
+    | TransparencyMode.all     => modify fun s => { s with cache.whnf := s.cache.whnf.insert ecck r }
     | _                        => unreachable!
   return r
 
diff --git a/Smt/Tactic/WHNFSmt.lean b/Smt/Tactic/WHNFSmt.lean
index 04801b7c..1fbc61d9 100644
--- a/Smt/Tactic/WHNFSmt.lean
+++ b/Smt/Tactic/WHNFSmt.lean
@@ -104,9 +104,8 @@ to let-lift `let-opaque` bindings. This can produce linearly-sized terms in cert
 
 Constants with names in `opaqueConsts` are also not unfolded. -/
 def smtOpaqueReduce (e : Expr) (opaqueConsts : Std.HashSet Name := {}) : MetaM Expr :=
-  withTheReader Meta.Context (fun ctx => { ctx with
-    canUnfold? := some (opaquePred opaqueConsts)
-  }) do Smt.reduce (skipTypes := false) e |>.run {
+  Meta.withCanUnfoldPred (opaquePred opaqueConsts) <|
+  Smt.reduce (skipTypes := false) e |>.run {
     letPushElim := true
   }
 
diff --git a/Smt/Translate/Commands.lean b/Smt/Translate/Commands.lean
index 5a0d2a1e..15dd1f83 100644
--- a/Smt/Translate/Commands.lean
+++ b/Smt/Translate/Commands.lean
@@ -29,15 +29,16 @@ inductive Command where
 
 namespace Command
 
-open Lean
-open Term
-open scoped Term.Notation
+open Lean Term
 
-def defNat : Command := .defineSort "Nat" [] (`"Int")
+def defNat : Command := .defineSort "Nat" [] (symbolT "Int")
 
 def defNatSub : Command :=
-  .defineFun "Nat.sub" [("x", `"Nat"), ("y", `"Nat")] (`"Nat")
-    (`"ite" • (`"<" • `"x" • `"y") • ``"0" • (`"-" • `"x" • `"y"))
+  .defineFun "Nat.sub" [("x", symbolT "Nat"), ("y", symbolT "Nat")] (symbolT "Nat")
+    (Term.mkApp3 (symbolT "ite")
+                 (Term.mkApp2 (symbolT "<") (symbolT "x") (symbolT "y"))
+                 (literalT "0")
+                 (Term.mkApp2 (symbolT "-") (symbolT "x") (symbolT "y")))
     false
 
 open ToSexp in
diff --git a/Smt/Translate/Term.lean b/Smt/Translate/Term.lean
index f62a737d..5d6d3393 100644
--- a/Smt/Translate/Term.lean
+++ b/Smt/Translate/Term.lean
@@ -31,24 +31,15 @@ inductive Term where
   deriving Inhabited
 
 namespace Term
-namespace Notation
-
-scoped infixl:20 " • "  => appT
-scoped prefix:21 " ` "  => symbolT
-scoped prefix:21 " `` " => literalT
-
-end Notation
-
-open scoped Notation
 
 def mkApp2 (f a b : Term) : Term :=
-  f • a • b
+  appT (appT f a) b
 
 def mkApp3 (f a b c : Term) : Term :=
-  f • a • b • c
+  appT (appT (appT f a) b) c
 
 def mkApp4 (f a b c d : Term) : Term :=
-  f • a • b • c • d
+  appT (appT (appT (appT f a) b) c) d
 
 /-- SMT-LIBv2 quoting for symbols. -/
 def quoteSymbol (s : String) : String :=
diff --git a/Test/Auto.expected b/Test/Auto.expected
index e69de29b..fdf406b4 100644
--- a/Test/Auto.expected
+++ b/Test/Auto.expected
@@ -0,0 +1,4 @@
+Test/Auto.lean:38:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!9 (!13 (!1 !2)) !3) = (!0 (!1 !2) !3)) is not type correct
+Test/Auto.lean:41:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!6 (!11 (!1 (!2 !3))) !3) = (!0 (!1 (!2 !3)) !3)) is not type correct
+Test/Auto.lean:44:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!6 (!10 (!1 (!2 !3))) !3) = (!0 (!1 (!2 !3)) !3)) is not type correct
+Test/Auto.lean:48:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!6 (!10 !1) (!2 (!3 !1))) = (!0 !1 (!2 (!3 !1)))) is not type correct
diff --git a/Test/BitVec/Shift.expected b/Test/BitVec/Shift.expected
index 88005d8d..9d781ffb 100644
--- a/Test/BitVec/Shift.expected
+++ b/Test/BitVec/Shift.expected
@@ -1,16 +1,16 @@
 goal: x ++ y = zeroExtend 4 x <<< 2#2 ||| zeroExtend 4 y
 
 query:
-(declare-const x (_ BitVec 2))
 (declare-const y (_ BitVec 2))
+(declare-const x (_ BitVec 2))
 (assert (distinct (concat x y) (bvor (bvshl ((_ zero_extend 2) x) #b10) ((_ zero_extend 2) y))))
 (check-sat)
 Test/BitVec/Shift.lean:5:8: warning: declaration uses 'sorry'
 goal: x ++ y = zeroExtend 6 x <<< 3#2 ||| zeroExtend 6 y
 
 query:
-(declare-const x (_ BitVec 3))
 (declare-const y (_ BitVec 3))
+(declare-const x (_ BitVec 3))
 (assert (distinct (concat x y) (bvor (bvshl ((_ zero_extend 3) x) #b11) ((_ zero_extend 3) y))))
 (check-sat)
 Test/BitVec/Shift.lean:10:8: warning: declaration uses 'sorry'
diff --git a/Test/BitVec/XorComm.expected b/Test/BitVec/XorComm.expected
index 9d49feaf..6cd4a967 100644
--- a/Test/BitVec/XorComm.expected
+++ b/Test/BitVec/XorComm.expected
@@ -1,8 +1,8 @@
 goal: x ^^^ y = y ^^^ x
 
 query:
-(declare-const x (_ BitVec 2))
 (declare-const y (_ BitVec 2))
+(declare-const x (_ BitVec 2))
 (assert (distinct (bvxor x y) (bvxor y x)))
 (check-sat)
 Test/BitVec/XorComm.lean:3:8: warning: declaration uses 'sorry'
diff --git a/Test/Int/Binders.expected b/Test/Int/Binders.expected
index 151a05d0..81f54980 100644
--- a/Test/Int/Binders.expected
+++ b/Test/Int/Binders.expected
@@ -2,8 +2,8 @@ goal: curryAdd a b = curryAdd b a
 
 query:
 (define-fun curryAdd ((a._@.Test.Int.Binders._hyg.4 Int) (a._@.Test.Int.Binders._hyg.6 Int)) Int (+ a._@.Test.Int.Binders._hyg.4 a._@.Test.Int.Binders._hyg.6))
-(declare-const b Int)
 (declare-const a Int)
+(declare-const b Int)
 (assert (distinct (curryAdd a b) (curryAdd b a)))
 (check-sat)
 Test/Int/Binders.lean:5:0: warning: declaration uses 'sorry'
@@ -11,15 +11,15 @@ goal: partCurryAdd a b = partCurryAdd b a
 
 query:
 (define-fun partCurryAdd ((a Int) (a._@.Test.Int.Binders._hyg.36 Int)) Int (+ a a._@.Test.Int.Binders._hyg.36))
-(declare-const b Int)
 (declare-const a Int)
+(declare-const b Int)
 (assert (distinct (partCurryAdd a b) (partCurryAdd b a)))
 (check-sat)
 Test/Int/Binders.lean:11:0: warning: declaration uses 'sorry'
 goal: partCurryAdd' a b = partCurryAdd' b a
 
 query:
-(define-fun |partCurryAdd'| ((a Int) (a._@.Init.Prelude._hyg.2519 Int)) Int (+ a a._@.Init.Prelude._hyg.2519))
+(define-fun |partCurryAdd'| ((a Int) (a._@.Init.Prelude._hyg.2531 Int)) Int (+ a a._@.Init.Prelude._hyg.2531))
 (declare-const a Int)
 (declare-const b Int)
 (assert (distinct (+ a b) (+ b a)))
diff --git a/Test/Int/DefineSort.expected b/Test/Int/DefineSort.expected
index 9c64cdd6..15e6649e 100644
--- a/Test/Int/DefineSort.expected
+++ b/Test/Int/DefineSort.expected
@@ -3,8 +3,8 @@ goal: a.add b = b.add a
 query:
 (define-sort MyInt () Int)
 (define-fun MyInt.add ((a MyInt) (b MyInt)) MyInt (+ a b))
-(declare-const b MyInt)
 (declare-const a MyInt)
+(declare-const b MyInt)
 (assert (distinct (MyInt.add a b) (MyInt.add b a)))
 (check-sat)
 Test/Int/DefineSort.lean:6:0: warning: declaration uses 'sorry'
diff --git a/Test/Int/DvdTimeout.expected b/Test/Int/DvdTimeout.expected
index 4a02b854..04fd6ed3 100644
--- a/Test/Int/DvdTimeout.expected
+++ b/Test/Int/DvdTimeout.expected
@@ -1,9 +1,9 @@
 goal: dvd a (b + c + d) = true
 
 query:
-(declare-const a Int)
-(declare-fun dvd (Int Int) Bool)
 (declare-const d Int)
+(declare-fun dvd (Int Int) Bool)
+(declare-const a Int)
 (assert (= (dvd a d) true))
 (declare-const c Int)
 (assert (= (dvd a c) true))
@@ -19,4 +19,4 @@ h1 : dvd a b = true
 h2 : dvd a c = true
 h3 : dvd a d = true
 ⊢ dvd a (b + c + d) = true
-Test/Int/DvdTimeout.lean:13:33: error: unexpected token '(timeout :='; expected command
+Test/Int/DvdTimeout.lean:13:33: error: unexpected token '('; expected command
diff --git a/Test/Nat/Cong.expected b/Test/Nat/Cong.expected
index e378911e..8b8560db 100644
--- a/Test/Nat/Cong.expected
+++ b/Test/Nat/Cong.expected
@@ -3,7 +3,7 @@ goal: x = y → f x = f y
 query:
 (define-sort Nat () Int)
 (declare-fun f (Nat) Nat)
-(assert (forall ((_uniq.965 Nat)) (=> (>= _uniq.965 0) (>= (f _uniq.965) 0))))
+(assert (forall ((_uniq.970 Nat)) (=> (>= _uniq.970 0) (>= (f _uniq.970) 0))))
 (declare-const y Nat)
 (assert (>= y 0))
 (declare-const x Nat)
diff --git a/Test/Nat/Max.expected b/Test/Nat/Max.expected
index d65a6ede..5a333d7d 100644
--- a/Test/Nat/Max.expected
+++ b/Test/Nat/Max.expected
@@ -2,12 +2,12 @@ goal: x ≤ x.max' y ∧ y ≤ x.max' y
 
 query:
 (define-sort Nat () Int)
-(declare-fun |Nat.max'| (Nat Nat) Nat)
-(assert (forall ((_uniq.1382 Nat)) (=> (>= _uniq.1382 0) (forall ((_uniq.1383 Nat)) (=> (>= _uniq.1383 0) (>= (|Nat.max'| _uniq.1382 _uniq.1383) 0))))))
-(declare-const y Nat)
-(assert (>= y 0))
 (declare-const x Nat)
 (assert (>= x 0))
+(declare-const y Nat)
+(assert (>= y 0))
+(declare-fun |Nat.max'| (Nat Nat) Nat)
+(assert (forall ((_uniq.1389 Nat)) (=> (>= _uniq.1389 0) (forall ((_uniq.1390 Nat)) (=> (>= _uniq.1390 0) (>= (|Nat.max'| _uniq.1389 _uniq.1390) 0))))))
 (assert (not (and (<= x (|Nat.max'| x y)) (<= y (|Nat.max'| x y)))))
 (check-sat)
 goal: x ≤ x.max' y ∧ y ≤ x.max' y
@@ -15,10 +15,10 @@ goal: x ≤ x.max' y ∧ y ≤ x.max' y
 query:
 (define-sort Nat () Int)
 (define-fun |Nat.max'| ((x Nat) (y Nat)) Nat (ite (<= x y) y x))
-(assert (forall ((_uniq.2960 Nat)) (=> (>= _uniq.2960 0) (forall ((_uniq.2961 Nat)) (=> (>= _uniq.2961 0) (>= (|Nat.max'| _uniq.2960 _uniq.2961) 0))))))
-(declare-const x Nat)
-(assert (>= x 0))
+(assert (forall ((_uniq.2978 Nat)) (=> (>= _uniq.2978 0) (forall ((_uniq.2979 Nat)) (=> (>= _uniq.2979 0) (>= (|Nat.max'| _uniq.2978 _uniq.2979) 0))))))
 (declare-const y Nat)
 (assert (>= y 0))
+(declare-const x Nat)
+(assert (>= x 0))
 (assert (not (and (<= x (|Nat.max'| x y)) (<= y (|Nat.max'| x y)))))
 (check-sat)
diff --git a/Test/Nat/ZeroSub'.expected b/Test/Nat/ZeroSub'.expected
index af15e979..8bc2a63c 100644
--- a/Test/Nat/ZeroSub'.expected
+++ b/Test/Nat/ZeroSub'.expected
@@ -1,6 +1,6 @@
 Test/Nat/ZeroSub'.lean:6:12: error: tactic 'assumption' failed
 case zero
-_uniq✝⁴⁰²⁻⁰ : ¬0 ≠ 0
+_uniq✝⁴⁰⁷⁻⁰ : ¬0 ≠ 0
 ⊢ ¬Smt.Reconstruct.andN' [] ¬0 - 0 = 0
 Test/Nat/ZeroSub'.lean:7:17: error: application type mismatch
   HAdd.hAdd x
diff --git a/Test/String/Length.expected b/Test/String/Length.expected
index b332e098..71159963 100644
--- a/Test/String/Length.expected
+++ b/Test/String/Length.expected
@@ -3,6 +3,6 @@ goal: "a".length = 1
 query:
 (define-sort Nat () Int)
 (declare-fun String.length (String) Nat)
-(assert (forall ((_uniq.786 String)) (>= (String.length _uniq.786) 0)))
+(assert (forall ((_uniq.791 String)) (>= (String.length _uniq.791) 0)))
 (assert (distinct (String.length "a") 1))
 (check-sat)
diff --git a/lake-manifest.json b/lake-manifest.json
index 67a32a8e..05618bf2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,47 +5,47 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84",
+   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/abdoo8080/lean-cvc5.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9ec3715a67cef65073b46a22e7807ecd783d9e12",
+   "rev": "38d6917e5ed4b5f87c1ba601bcd8f3cc201397fd",
    "name": "cvc5",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "9ec3715",
+   "inputRev": "38d6917",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fa3040aa203ea9d88ae958fab0fca8284c3640de",
+   "rev": "128b0975d262992d69d02a60e3b5728a85bc3297",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "fa3040aa203ea9d88ae958fab0fca8284c3640de",
+   "inputRev": "128b0975d262992d69d02a60e3b5728a85bc3297",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,57 +55,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7",
+   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68280daef58803f68368eb2e53046dabcd270c9d",
+   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.47",
+   "inputRev": "v0.0.48",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
index bb024d6c..795c6d34 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -3,13 +3,13 @@ import Lake
 open Lake DSL
 
 require auto from
-  git "https://github.com/leanprover-community/lean-auto.git" @ "fa3040aa203ea9d88ae958fab0fca8284c3640de"
+  git "https://github.com/leanprover-community/lean-auto.git" @ "128b0975d262992d69d02a60e3b5728a85bc3297"
 
 require cvc5 from
-  git "https://github.com/abdoo8080/lean-cvc5.git" @ "9ec3715"
+  git "https://github.com/abdoo8080/lean-cvc5.git" @ "38d6917"
 
 require mathlib from
-  git "https://github.com/leanprover-community/mathlib4.git" @ "v4.14.0"
+  git "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"
 
 package smt
 
diff --git a/lean-toolchain b/lean-toolchain
index 1e70935f..d0eb99ff 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0
+leanprover/lean4:v4.15.0